Executable Behaviour and the pi-Calculus

Reactive Turing machines extend classical Turing machines with a facility to model observable interactive behaviour. We call a behaviour executable if, and only if, it is behaviourally equivalent to the behaviour of a reactive Turing machine. In this paper, we study the relationship between executable behaviour and behaviour that can be specified in the πcalculus. We establish that all executable behaviour can be specified in the π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 πcalculus allows the specification of behaviour that is not executable up to divergence-preserving branching bisimilarity. Motivated by an intuitive understanding of executability, we then consider a restriction on the operational semantics of the πcalculus that does associate with every π-term executable behaviour, at least up to the version of branching bisimilarity that does not require the preservation of divergence.