Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Type abstractions of name-passing processes
Lucia Acciai, Michele Boreale
abstract:
We study methods to statically approximate "first-order" process calculi (Pi, Join) by "propositional" models (CCS, BPP, Petri nets). We consider both open and closed behaviors of processes. In the case of open behavior, we propose a type system to associate pi-calculus processes with restriction-free CCS types. A process is shown to be in simulation relation with each of its types, hence safety properties that hold of the types also hold of the process. We refine this approach in the case of closed behavior: in this case, types are BPP processes. Sufficient conditions are given under which a minimal BPP type can be computed that is bisimilar to a given process. These results are extended to the Join calculus using place/transition Petri nets as types.
