Two-way automata: limitations and frontiers

对自然现象的洞察使人类能够与自然进行富有成效的互动。同样，在计算机科学中，理解系统和软件操作背后的基本原理可以更好地解决用户的问题。现代软件系统庞大、复杂，并且经常出现错误和故障。根据应用领域的不同，这些可能是良性的，也可能花费数千甚至数百万英镑（例如，英国邮政丑闻中的赔偿和法律的费用[1]）。对形式验证的研究旨在降低这些成本。为了应对不断增长的规模和复杂性，可以对系统进行验证：简而言之，验证可以以数学确定性证明系统的行为符合预期，并且没有表现出不良行为（崩溃，故障等）。所需的保证由用户或客户指定。在软件的开发和维护过程中，通常需要处理的不是同一系统的一个版本，而是多个版本。解决办法是使验证--根据用户给出的规范--自动化，即，由专用的计算机工具执行。这种范例被称为模型检查：验证工具提供了实际系统或软件的数学模型。模型检验为Clarke、Emerson和Sifakis赢得了2007年的图灵奖（“诺贝尔计算机奖”）。模型检测的核心是对系统和软件的简单但功能强大的模型的行为的洞察，传统上称为“自动机”。不幸的是，验证算法的计算复杂度随着系统规模的增加而迅速增加，并且通常非常高。为了能够将验证扩展到越来越大的系统，需要定制模型检查：根据待验证系统的性质，需要使用不同类型的自动机作为模型。了解各种自动机对于可扩展性验证至关重要。本项目将研究一个称为“双向有限自动机”的自动机族，因为“阅读头”的向前和向后运动是其显著特征。这个系列的重要性在于它们与许多其他模型的联系：关于双向自动机的算法见解与扩展多种现有验证技术的范围的潜力紧密相关。新的见解可以为无处不在的编程习惯和范式（例如，处理列表和字符串，以及在子例程中构造软件源代码）。我们将攻击双向自动机上三个长期存在的开放问题，目的是通过识别这些自动机的基本限制来揭示这些新的见解。我们希望这次攻击至少解决这三个问题中的一个（可能更多，受益于三个工作流之间的协同作用），并在所有三个方面推进前沿。我们将利用双向自动机的局限性，开发新的和更可扩展的验证算法。[1]https://en.wikipedia.org/wiki/British_Post_Office_scandal

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