A Decidable Characterization of a Graphical Pi-calculus with Iterators

TL;DR

This paper introduces Pi-graphs, a visual and graphical Pi-calculus variant with iterators, enabling decidable bisimilarity verification for modeling and analyzing mobile systems.

Contribution

It provides a decidable characterization of a graphical Pi-calculus with iterators, facilitating verification of non-terminating mobile system behaviors.

Findings

Bisimilarity is decidable for Pi-graphs.

Ground notions of labelled transition and bisimulation are used.

Automatic garbage collection of unused names supports decidability.

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.