Top of this page
Skip navigation, go straight to the content

Ph.D. Thesis

I will defend my thesis entitled From Computability to Executability – A process-theoretic view on automata theory on Thursday 27 October 2011 at 16:00 in room 5 of the Auditorium. For more information about the defence, check the information page.

My Ph.D. supervisors are Jos Baeten (promotor) and Bas Luttik (co-promotor). The work in this thesis has been carried out under the auspices of the research school IPA (Institute for Programming research and Algorithmics). I am supported by NWO (the Netherlands Organisation for Scientific Research), project "Models of Computation: Automata and Processes’’ (nr. 612.000.630).

The following versions of the thesis are available for download:

Related downloads:

Cover design by Sofie van Schadewijk; extensive review by Alexandra Silva, Bas Luttik, Bram Senders, and Jos Baeten.

Short Summary

The theory of automata and formal languages was devised in the 1930s to provide models for and to reason about computation. Here we mean by computation a procedure that transforms input into output, which was the sole mode of operation of computers at the time. Nowadays, computers are systems that interact with us and also with each other; they are non-deterministic, reactive systems. Concurrency theory, split off from classical automata theory in the seventies, provides a model of computation similar to the model given by the theory of automata and formal languages, but focuses on concurrent, reactive and interactive systems.

This thesis investigates the integration of the two theories, exposing the differences and similarities between them. Where automata and formal language theory focuses on computations and languages, concurrency theory focuses on behaviour. To achieve integration, we look for process-theoretic analogies of classic results from automata theory. The most prominent difference is that we use an interpretation of automata as labelled transition systems modulo (divergence-preserving) branching bisimilarity instead of treating automata as language acceptors. We also consider similarities such as grammars as recursive specifications and finite automata as labelled finite transition systems. We investigate whether the classical results still hold and, if not, what extra conditions are sufficient to make them hold.

We especially look into three levels of Chomsky’s hierarchy: we study the notions of finite-state systems, pushdown systems, and computable systems. Additionally we investigate the notion of parallel pushdown systems. For each class we define the central notion of automaton and its behaviour by associating a transition system with the automaton. Then we introduce a suitable specification language and investigate the correspondence with the respective automaton (via its associated transition system). Because we not only want to study interaction with the environment, but also the interaction within the automaton, we make the interaction explicit by means of communicating parallel components, with one component representing the finite control of the automaton and one component representing the memory.