文章基本信息

标题：The π-Calculus is Behaviourally Complete and Orbit-Finitely Executable
本地全文：下载
作者：Yang, Fei ; Luttik, Bas
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2021
卷号：17
期号：1
页码：1-26
语种：English
出版社：Technical University of Braunschweig
摘要：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.
关键词：Computer Science - Logic in Computer Science