A Theory of Executability: with a Focus on the Expressivity of Process Calculi
Fei Yang
first promotor: prof. dr. J.C.M. Baeten (TU/e)
second promoter: prof. dr. ir. J.F Groote (TU/e)
copromotor: dr. S.P. Luttik (TU/e)
Eindhoven University of Technology
Date: 11 June 2018
Thesis: PDF
Summary
Computability theory and concurrency theory are two of the fundamental research areas in theoretical computer science. Computability theory studies the computational power of computing systems in terms of functions on natural numbers. Many models of computation, e.g., Turing machines, recursive functions, lambda calculus, etc., were shown to be equivalent. Such equivalences provide evidence for the famous Church-Turing thesis, which could be phrased as: “a function on the natural numbers is computable by an algorithm, ignoring resource limitations, if and only if it is computable by a Turing machine.”
Computability theory does not address the aspect of interaction between systems. In order to study interaction between systems, concurrency theory was proposed. In concurrency theory, the behaviour of a system is mathematically represented as a labelled transition system. To specify and reason about labelled transition systems, many process calculi have been proposed. The community of concurrency theory developed a large variety of methods to measure the expressivity of process calculi. We address a natural question whether we can use the knowledge in computability theory to evaluate the expressivity of process calculi.
In this thesis, we study a theory of executability, which is the integration of computability theory and concurrency theory. It is based on Reactive Turing Machines (RTMs), concurrent variants of Turing machines. Every RTM has an associated labelled transition system. The labelled transition system semantics allows us to define that a transition system is executable when it is behaviourally equivalent to the transition system associated with an RTM. In concurrency theory, there are many behavioural equivalences, differing in the behavioural properties they preserve. From the perspective of expressivity, it is convenient to consider behavioural equivalence as a parameter of the theory of executability. We aim for results modulo divergence-preserving branching bisimilarity, which is the finest known behavioural equivalence in van Glabbeek’s spectrum of equivalences.
In Chapter 2 of the thesis, we first provide some preliminaries for the theory of executability, including the definitions and some basic lemmas about RTMs and executable behaviours. In particular, the role of divergence is discussed, since divergence plays a significant role in the theory of executability. Moreover, a framework of expressivity is proposed. The theory of executability could be applied to measure the expressivity of a process calculus in two aspects. One is the executability, that is, whether every transition system specified in the process calculus is executable modulo some behavioural equivalence; the other one is the reactive Turing powerfulness, that is, whether every executable transition system could be specified in the process calculus modulo some behavioural equivalence.
This thesis proceeds to contribute to four topics in the theory of executability.
Chapter 3 of the thesis gives some evidence for the robustness of executability theory based on RTMs. A comparison is made between RTMs and Interactive Turing Machines (ITMs). An ITM is a model of interactive computation invented by van Leeuwen and Wiedermann. It models interactive computation as a translation over infinite streams. We show that RTMs are at least as expressive as ITMs, both with respect to its semantics in terms of labelled transition systems modulo divergence-preserving branching bisimilarity and also with respect to its semantics in terms of stream translations. For ITMs, van Leeuwen and Wiedermann proposed an extension with a notion of advice, allowing them to model evolving systems such as the Internet. We show that such an extension can also be defined for RTMs.
Chapter 4 of the thesis aims to make some revision of concurrency theory in the context of executability theory. The chapter addresses the semantics of sequential composition in a calculus with intermediate termination. We identify two problems with the standard semantics, namely unbounded branching and forgetfulness. Two issues have been considered in this chapter in the presence of intermediate termination, namely, the relationship between pushdown processes and context-free processes, and the reactive Turing powerfulness of a process calculus with the nesting operator. We cannot resolve unbounded branching and forgetfulness in the classical operational semantics due to transparency. For this reason, we cannot answer the two issues above. We propose a revised semantics of the sequential composition operator in the presence of intermediate termination. In the revised semantics, transparency is eliminated. Thus, we resolve the two problems above in the revised semantics. We show that every context-free process can be simulated by a pushdown process modulo strong bisimilarity, and the process calculus with a nesting operator is reactively Turing powerful modulo branching bisimilarity.
Chapter 5 of the thesis applies the theory of executability to evaluate the expressivity of the π-calculus. The π-calculus is a widely used process calculus, and its expressivity has been studied extensively in the literature. Most of the results about the expressivity of the π-calculus are about its relative expressivity, that is, the expressivity compared to some other calculus. In the theory of executability, we investigate its absolute expressivity, that is, whether a transition system specified in the π-calculus can be executed by an interactive computing system or not. We show that the π-calculus is reactively Turing powerful modulo divergence-preserving branching bisimilarity. It is not executable since the transition systems associated with π-calculus processes are not limited to a finite set of labels whereas an RTM only accept a finite set of action labels. We investigate the executability of π-calculus by making a compromise that restricts the transition systems associated with π-calculus processes referring to only finitely many names. We show that the π-calculus is executable in the restricted semantics modulo a divergence-insensitive variant of branching bisimilarity.
Chapter 6 of the thesis tries to adapt the theory of executability to a broader domain. In order to apply executability theory to evaluate expressivity of process calculi with infinite alphabets such as the π-calculus, mCRL2 and the value-passing calculus, we extend the theory on the dimension of the infinity of the alphabet. We first propose a notion of an infinitary RTM that allows the sets in the definition of an RTM to be countable. However, it turns out that such an extension hardly makes any sense since every countable transition system is then simply executable. Then, we make some attempts to restrict the transition relation in the RTMs to be effective or computable, which leads to two slightly better notions of executability. Finally, we introduce a theory of nominal executability by using sets with atoms in the definition of RTMs. In the theory of nominal executability, there are two requirements imposed on sets with atoms, namely, legality and hereditary orbit-finiteness. These two requirements do not restrict a set to finitely many elements and still keep the set definable by finitely many elements with finitely many orbits modulo permutation of atoms. We show that the π-calculus is nominally executable modulo a divergence-insensitive variant of branching bisimilarity, but mCRL2 is not. Hence, we have some evidence that the theory of nominal executability is a meaningful notion in the study of expressivity.
Chapter 7 concludes the thesis and proposes some future directions in the research of executability theory. Firstly, there are many models for interactive computation in the literature. Comparing them with RTMs would gain more evidence for the robustness of executability theory. Secondly, an integration of complexity theory and concurrency theory can be an interesting extension of executability theory. Thirdly, the process calculus with the revised sequential composition operator still lacks an axiomatization. Fourthly, the relationship between pushdown processes and context-free processes is still unclear in the classical semantics. Fifthly, the reactive Turing powerfulness of many process calculi using non-regular iterators other than the nesting operator still needs to be proved. Sixthly, the extensions of RTMs could still be exploited in two dimensions, the choice of advice and the choice of infiniteness.
As a conclusion, the thesis results in some basic building blocks for a theory of executability, namely, the robustness of RTMs, the revision in concurrency theory, the evaluation of expressivity, and the extension of a theory of executability. A step has been made towards a concurrent version of the Church-Turing thesis.