Two-way automata: limitations and frontiers

Insights about natural phenomena enable humankind to interact with nature fruitfully. Similarly, in computer science, understanding the fundamental principles behind the operation of systems and software leads to better solutions to users' problems. Modern software systems are big, complex, and often exhibit bugs and faults. Depending on the application domain, these can be benign or they can cost thousands and even millions of pounds (as, for example, compensation and legal costs awarded in the British Post Office scandal [1]). Research on formal verification is aimed at reducing these costs. To tackle the growing size and complexity, systems can be verified: in a nutshell, verification makes it possible to prove, with mathematical certainty, that systems behave in accordance with expectation and exhibit no undesirable behaviours (crashes, faults, etc.). The desired guarantees are specified by the user or customer. Often not one but multiple versions of the same system need to be handled, during the development and maintenance of software. The solution is to make verification -- against a specification given by the user -- automated, i.e., carried out by a dedicated computer tool. This paradigm is referred to as model checking: the verification tool is supplied a mathematical model of the actual system or software. Model checking won Clarke, Emerson, and Sifakis a Turing award ("the Nobel prize of computing") in 2007. At the core of model checking are insights about the behaviour of simple but powerful models of systems and software, traditionally called "automata".

Unfortunately, the computational complexity of verification algorithms increases rapidly with the system size and is often prohibitively high. To make it possible to scale the verification up to bigger and bigger systems, model checking needs to be tailored: depending on the nature of a system to be verified, different types of automata need to be used as models. Insights about various automata are crucial for scalable verification.

This project will study a family of automata known as "two-way finite automata", for the distinguishing feature of forward and backward movement of the "reading head". The importance of this family lies in their connections with numerous other models: algorithmic insights about two-way automata are tightly linked to the potential to expand the scope of multiple existing verification techniques. New insights can lead to faster verification algorithms for ubiquitous programming idioms and paradigms (e.g., processing lists and strings, and structuring software source code in subroutines). We will attack three longstanding open problems on two-way automata, with the aim to uncover such new insights, by identifying fundamental limitations of these automata. We expect this attack to resolve at least one of these three problems (possibly more, benefitting from the synergy between the three streams of work) and to advance the frontier on all three. We will exploit the limitations of two-way automata to develop new and more scalable verification algorithms.

[1] https://en.wikipedia.org/wiki/British_Post_Office_scandal