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.

The aim of the project is to devise tools and algorithms to help with the design, analysis, and verification of complex computer systems, particularly those arising in novel application domains. The ultimate beneficiaries of this research will include system designers and users. As detailed in the case for support, the counter automata models that we consider are already used in analysis of cryptographic protocols, intrusion detection, linked data structures, XML querying, recursive procedures, and unbounded concurrency (amongst many others).

The models that we consider in the proposal already enjoy industrial-strength tool support, including UPPAAL for timed systems, or LoLA for Petri nets. The new algorithms that we propose to develop have the potential to enhance substantially the capability of subsequent versions of such tools. We plan a workshop that will bring together algorithm designers and tool builders to help explain our ideas and to cross-fertilise with developments of other research groups.

A significant part of the project concerns decision procedures for extensions of Presburger arithmetic that can express divisibility. To help mediate the impact of this we will produce an open-source tool for solver for quantifier-free constraints in this logic. While there exist several widely used computational engines for solving linear arithmetic constraints (Z3, Yices, etc.) , there is much less support for non-linear constraints. In this respect, we believe our tool will advance the state of the art and will influence the next generation of SMT solvers.