On Hierarchical Communication Topologies in the pi-calculus

TL;DR

This paper introduces a static analysis method for verifying hierarchical communication topologies in pi-calculus terms, enabling decidable safety verification for a significant fragment of the calculus.

Contribution

It presents a novel type system for automatically inferring hierarchy invariants in pi-calculus terms, proving their soundness and decidability of coverability.

Findings

The type system can automatically prove hierarchy invariants.

Coverability is decidable for hierarchical pi-terms.

Hierarchical pi-terms are depth-bounded, ensuring safety properties.

Abstract

This paper is concerned with the shape invariants satisfied by the communication topology of {\pi}-terms, and the automatic inference of these invariants. A {\pi}-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 {\pi}-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 {\pi}-calculus with decidable safety verification problems.