Counter Automata: Verification and Synthesis

反自动机是一种通用的计算模型，自计算机科学成立以来一直在研究。特别是，反自动机在自动验证中得到了深入的研究，因为它们可以自然地模拟各种计算特征，如链接数据结构、递归和无界并行性。然而，这种灵活性和表现力使得他们的算法分析非常具有挑战性。该项目的目标是开发新的自动化程序来分析反自动机，最终将有助于复杂计算机系统的设计、建模、验证和分析。项目的一般领域是模型检查，这是设计复杂硬件和软件系统问题的一种方法。本质上，模型检查涉及系统抽象数学模型的构建和系统分析，理想情况下是在设计时使用自动化工具。面对云计算、并发嵌入式系统、多核硬件、物联网、大数据等新技术带来的挑战，该领域的重要性与日俱增。在许多应用领域中，计算机系统的有效设计和正确运行在经济和安全上都是至关重要的。2007年的图灵奖授予了Clarke、Emerson和Sifakis，以表彰他们在该领域的基础性工作，表彰了模型检查的重要性和科学挑战。本提案旨在通过开发反自动机的算法和分析工具来丰富模型检查的工具包。固有的主要科学挑战之一是模型检查涉及对模型的状态空间进行详尽的分析，而反自动机本质上是具有通用计算能力的无限状态设备。另一个重大挑战是，我们将考虑具有附加特征的反自动机，例如参数和概率行为。为了迎接这一挑战，我们将建立在过去二十年来发展起来的一系列技术之上，利用强大的抽象和丰富的逻辑理论，使我们能够以有限的方式象征性地表示和推理无限的状态空间。该项目的成果将包括帮助分析反自动机的新算法，以及解决此类分析中出现的算术约束的开源工具。已经有各种各样的高效工具用于分析反自动机，包括Petri网。我们的目标是，这笔拨款的成果将增强下一代这些工具的能力。

Counter automata are a universal computational model that has been studied since the inception of computer science. In particular, counter automata have been intensively studied in automated verification since they can naturally model diverse computational features such as linked data structures, recursion, and unbounded parallelism. This flexibility and expressiveness however makes their algorithmic analysis very challenging. The goal of this project is to develop new automated procedures for analysing counter automata that will ultimately aid the design, modelling, verification, and analysis of complex computer systems.The general area of the project is model checking, which is an approach to the problem of designing complex hardware and software systems. In essence, model checking involves the construction and systematic analysis of abstract mathematical models of systems, ideally at design time, using automated tools. The importance of the area is growing in response to the challenge posed by new technologies such as the cloud, concurrent embedded systems, multi-core hardware, the Internet of Things, Big Data, etc. In many application areas the efficient design and correct functioning of computer systems is both economically critical and safety critical. The significance and scientific challenge of model checking were recognized by bestowal of the 2007 Turing Award to Clarke, Emerson, and Sifakis for their foundational work in the area.This proposal aims to enrich the tool-kit of model checking by developing algorithms and analysis tools for counter automata. One of the major inherent scientific challenges is that model checking involves performing exhaustive analysis of the state spaces of models, whereas counter automata are inherently infinite-state devices that have universal computing power. Another significant challenge is that we will be considering counter automata with additional features, such as parameters and probabilistic behaviour. To meet this challenge we will build on a body of techniques developed over the past two decades, making use of powerful abstractions and rich logical theories of arithmetic which allow us symbolically to represent and reason about infinite state spaces in a finite way. Outcomes of the project will include new algorithms to help analyse counter automata as well as an open-source tool for solving arithmetic constraints that arise in such analysis. There is already a wide variety of highly effective tools for analysing counter automata, including Petri nets. Our goal is that the outcomes of this grant will enhance the capabilities of the next generation of these tools.