Reactive Turing machines extend Turing machines with a facility to model observable interactive behaviour. A behaviour is called 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 defined in the $\pi$-calculus. We establish that executable behaviour is definable in the $\pi$-calculus up to a fine notion of behavioural equivalence that preserves all moments of choice and divergence. Moreover, we exhibit behaviour definable in the $\pi$-calculus that is not executable up to divergence-preserving behavioural equivalence. We do, however, obtain that every behaviour definable in the $\pi$-calculus is executable up to a divergence-insensitive notion of behavioural equivalence.

Original language | English |
---|

Publisher | s.n. |
---|

Number of pages | 17 |
---|

Publication status | Published - 2014 |
---|

Name | arXiv |
---|

Volume | 1410.4512 [cs.LO] |
---|