Encoding Asynchronous Interactions Using Open Petri Nets

摘要

We present an encoding for (bound) processes of the asynchronous CCS with replication into open Petri nets: ordinary Petri nets equipped with a distinguished set of open, places. The standard token game of nets models the reduction semantics of the calculus; the exchange of tokens on open places models the interactions between processes and their environment. The encoding preserves strong and weak CCS asynchronous bisimilaritics: it thus represents a relevant step in establishing a precise correspondence between asynchronous calculi and (open) Petri nets. The work is intended as fostering the technology transfer between these formalisms: as an example, we discuss how some results on expressiveness can be transferred from the calculus to nets and back.