A compositional Petri net translation of general π -calculus terms

Formal Aspects of Computing - 2008
Raymond Devillers1, Hanna Klaudel2, Maciej Koutny3
1Département d’Informatique, Université Libre de Bruxelles CP212, 1050, Brussels, Belgium
2IBISC, FRE 2873 CNRS, Université d’Evry Val d’Essonne, 91000, Evry, France
3School of Computing Science, Newcastle University, NE1 7RU, Newcastle upon Tyne, UK

Tóm tắt

Abstract We propose a finite structural translation of possibly recursive π -calculus terms into Petri nets. This is achieved by using high-level nets together with an equivalence on markings in order to model entering into recursive calls, which do not need to be guarded. We view a computing system as consisting of a main program ( π -calculus term) together with procedure declarations (recursive definitions of π -calculus identifiers). The control structure of these components is represented using disjoint high-level Petri nets, one for the main program and one for each of the procedure declarations. The program is executed once, while each procedure can be invoked several times (even concurrently), each such invocation being uniquely identified by structured tokens which correspond to the sequence of recursive calls along the execution path leading to that invocation.

Từ khóa


Tài liệu tham khảo

10.5555/500774

10.1016/0304-3975(87)90090-9

10.1007/s002360050144

Boreale M Sangiorgi D (1995) A fully abstract semantics for causality in the π -calculus. In: Proceedings of STACS 1995. Springer Heidelberg LNCS vol 900 pp 243–254

Busi N Gorrieri R (1995) A Petri net semantics for π -calculus. In: Proceedings of CONCUR 1995 LNCS vol 962 pp 145–159

Cattani GL Sewell P (2000) Models for name-passing processes: interleaving and causal. In: Proceedings of LICS 2000. IEEE CS Press Los Alamitos pp 322–333

Cattani GL Sewell P (2000) Models for name-passing processes: interleaving and causal. Technical report TR-505 University of Cambridge Cambridge

Christensen S Hansen ND (1993) Coloured Petri nets extended with place capacities test arcs and inhibitor arcs. In: Proceedings of ICATPN 1993. Springer Heidelberg LNCS vol 691 pp 186–205

Devillers R Klaudel H (2004) Solving Petri net recursions through finite representation. In: Proceedings of IASTED 2004. ACTA Press New York pp 145–150

10.1016/j.entcs.2006.05.008

Devillers R, 2006, Petri net semantics of the finite π-calculus terms, Fundam Inf, 70, 1

Devillers R Klaudel H Koutny M (2006) A Petri net translation of π -calculus terms. ICTAC 2006 LNCS vol 4281 pp 138–152

10.1016/S0304-3975(02)00088-9

10.5555/2370756.2370757

10.1016/0304-3975(95)00118-2

Grahlmann B Best E (1996) PEP—more than a Petri net tool. In: Proceedings of TACAS 1996. Springer Heidelberg LNCS vol 1055 pp 397–401

Haddad S Poitrenaud D (2000) Modelling and analyzing systems with recursive Petri nets. In: Proceedings of WODES 2000. Kluwer Dordrecht pp 449–458

Khomenko V (2003) Model checking based on prefixes of Petri net unfoldings. Ph.D thesis School of Computing Science University of Newcastle

Kiehn A (1990) Petri net systems and their closure properties. In: Rozenberg G

(ed) Advances in Petri nets 1989. Springer Heidelberg LNCS vol 424 pp 306-328

Khomenko V Koutny M Niaouris A (2006) Applying Petri net unfoldings for verification of mobile systems. Technical report CS-TR-953 University of Newcastle. In: Post-proceedings of MOCA 2006 (to appear)

Milner R, 1989, Communication and concurrency

Mobility Workbench. Uppsala Universitet. http://www.it.uu.se/research/group/mobility/mwb

Montanari U Pistore M (1995) Concurrent semantics for the π -calculus. In: Proceedings of MFPS 1995 Electronic notes in computer science vol 1. Elsevier Amsterdam pp 1–19

Montanari U Pistore M (2001) History dependent automata. Technical report 0112-14 Instituto Trentino di Cultura

10.1016/0890-5401(92)90008-4

10.1016/B978-044482830-9/50026-6

Thông tin
Thông tin xuất bản

Formal Aspects of Computing

Thông tin tác giả