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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.39.4 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |