Executable behaviour and the $π$-calculus

B. Luttik, F. Yang

Research output: Book/ReportReportAcademic

48 Downloads (Pure)


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 languageEnglish
Number of pages17
Publication statusPublished - 2014

Publication series

Volume1410.4512 [cs.LO]

Fingerprint Dive into the research topics of 'Executable behaviour and the $π$-calculus'. Together they form a unique fingerprint.

Cite this