This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable from P satisfies a T -shaped invariant. We design a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of π-calculus reactions. The coverability problem for hierarchical terms is decidable. This is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the π-calculus with decidable safety verification problems.
CITATION STYLE
D’Osualdo, E., & Ong, C. H. L. (2016). On hierarchical communication topologies in the π-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9632, pp. 149–175). Springer Verlag. https://doi.org/10.1007/978-3-662-49498-1_7
Mendeley helps you to discover research relevant for your work.