摘要：Reactive Turing machines extend classical Turing machines with a facility tomodel 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 betweenexecutable behaviour and behaviour that can be specified in the π-calculus.We establish that every finitely executable behaviour can be specified in the π-calculus up to divergence-preserving branching bisimilarity. Theconverse, however, is not true due to (intended) limitations of the model ofreactive Turing machines. That is, the π-calculus allows the specificationof behaviour that is not finitely executable up to divergence-preservingbranching bisimilarity. We shall prove, however, that if the finitenessrequirement on reactive Turing machines and the associated notion ofexecutability is relaxed to orbit-finiteness, then the π-calculus isexecutable up to (divergence-insensitive) branching bisimilarity.
