Two-way automata: limitations and frontiers

双向自动机：局限性和边界

• 批准号: EP/X03027X/1
• 负责人: Dmitry Chistikov
• 金额: $ 35.73万
• 依托单位: University of Warwick
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FX03027X%2F1
• 关键词: Two; way; automata; limitations; 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

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