The $\pi$-Calculus is Behaviourally Complete and Orbit-Finitely Executable

TL;DR

This paper demonstrates that the $alculus can specify all finitely executable reactive behaviors and, under a relaxed orbit-finiteness condition, can represent behaviors executable up to divergence-insensitive branching bisimilarity.

Contribution

It establishes the behavioral completeness of the $alculus for finitely executable and orbit-finitely executable reactive behaviors, clarifying its expressive power relative to reactive Turing machines.

Findings

Every finitely executable behaviour can be specified in the alculus up to divergence-preserving branching bisimilarity.

The alculus can specify behaviors not finitely executable, due to model limitations.

Under orbit-finiteness, the alculus is executable up to divergence-insensitive branching bisimilarity.

Abstract

Reactive Turing machines extend classical Turing machines with a facility to model observable interactive behaviour. We call a behaviour (finitely) executable if, and only if, it is equivalent to the behaviour of a (finite) reactive Turing machine. In this paper, we study the relationship between executable behaviour and behaviour that can be specified in the $\pi$-calculus. We establish that every finitely executable behaviour can be specified in the $\pi$-calculus up to divergence-preserving branching bisimilarity. The converse, however, is not true due to (intended) limitations of the model of reactive Turing machines. That is, the $\pi$-calculus allows the specification of behaviour that is not finitely executable up to divergence-preserving branching bisimilarity. We shall prove, however, that if the finiteness requirement on reactive Turing machines and the associated notion of executability is relaxed to orbit-finiteness, then the $\pi$-calculus is executable up to (divergence-insensitive) branching bisimilarity.