Counter Automata: Verification and 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.