A Decidable Characterization of a Graphical Pi-calculus with Iterators
Formal Languages and Automata Theory
2010-11-02 v1 Logic in Computer Science
Abstract
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.
Cite
@article{arxiv.1011.0220,
title = {A Decidable Characterization of a Graphical Pi-calculus with Iterators},
author = {Frédéric Peschanski and Hanna Klaudel and Raymond Devillers},
journal= {arXiv preprint arXiv:1011.0220},
year = {2010}
}
Comments
In Proceedings INFINITY 2010, arXiv:1010.6112