A Decidable Characterization of a Graphical Pi-calculus with Iterators

Frédéric Peschanski
(UPMC-LIP6)
Hanna Klaudel
(Université Evry-Ibisc)
Raymond Devillers
(Université Libre de Bruxelles)

This paper presents the Pi-graphs, a visual paradigm for the modelling and verification of mobile systems. The language is a graphical variant of the Pi-calculus with iterators to express non-terminating behaviors. The operational semantics of Pi-graphs use ground notions of labelled transition and bisimulation, which means standard verification techniques can be applied. We show that bisimilarity is decidable for the proposed semantics, a result obtained thanks to an original notion of causal clock as well as the automatic garbage collection of unused names.

In Yu-Fang Chen and Ahmed Rezine: Proceedings 12th International Workshop on Verification of Infinite-State Systems (INFINITY 2010), Singapore, 21st September 2010, Electronic Proceedings in Theoretical Computer Science 39, pp. 47–61.
Published: 28th October 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.39.4 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org