### Abstract

Original language | English |
---|---|

Pages (from-to) | 37-52 |

Journal | Electronic Proceedings in Theoretical Computer Science |

Issue number | 189 |

DOIs | |

Publication status | Published - 2015 |

### Fingerprint

### Bibliographical note

PT: J; NR: 19; TC: 0; J9: ELECTRON PROC THEOR; PG: 16; GA: CZ8GW; UT: WOS:000367339200004### Cite this

*Electronic Proceedings in Theoretical Computer Science*, (189), 37-52. https://doi.org/10.4204/EPTCS.189.5

}

*Electronic Proceedings in Theoretical Computer Science*, no. 189, pp. 37-52. https://doi.org/10.4204/EPTCS.189.5

**Executable Behaviour and the pi-Calculus.** / Luttik, B.; Yang, F.

Research output: Contribution to Journal › Article › Academic › peer-review

TY - JOUR

T1 - Executable Behaviour and the pi-Calculus

AU - Luttik, B.

AU - Yang, F.

N1 - PT: J; NR: 19; TC: 0; J9: ELECTRON PROC THEOR; PG: 16; GA: CZ8GW; UT: WOS:000367339200004

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

U2 - 10.4204/EPTCS.189.5

DO - 10.4204/EPTCS.189.5

M3 - Article

SP - 37

EP - 52

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

IS - 189

ER -