Counter Automata: Verification and Synthesis

计数器自动机：验证与综合

• 批准号: EP/M012298/1
• 负责人: James Worrell
• 金额: $ 30.78万
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2015
• 资助国家: 英国
• 起止时间: 2015 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FM012298%2F1
• 关键词: Counter; Automata; Verification; Synthesis

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.

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

项目成果

Pumping lemmas for weighted automata

加权自动机的泵送引理

• DOI: 10.46298/lmcs-17(3:7)2021
• 发表时间: 2021
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Chattopadhyay A

Probabilistic automata of bounded ambiguity

有界模糊性的概率自动机

• DOI: 10.4230/lipics.concur.2017.19
• 发表时间: 2017
• 期刊: Leibniz International Proceedings in Informatics, LIPIcs
• 作者: Fijalkow, N.

On matrix powering in low dimensions

低维矩阵供电

• DOI: 10.4230/lipics.stacs.2015.329
• 发表时间: 2015
• 期刊: Leibniz International Proceedings in Informatics, LIPIcs
• 作者: Galby E

The Polyhedron-Hitting Problem

多面体撞击问题

• DOI: 10.1137/1.9781611973730.64
• 发表时间: 2015
• 作者: Chonev V

Complexity of Two-Variable Logic on Finite Trees

• DOI: 10.1145/2996796
• 发表时间: 2013-07
• 期刊: ACM Transactions on Computational Logic (TOCL)
• 作者: Saguy Benaim;Michael Benedikt;Witold Charatonik;Emanuel Kieronski;R. Lenhardt;Filip Mazowiecki;J. Worrell-J.-Wo