A generic transducer-based approach to modelling and verifying infinite systems

Computers have become so complex today that the likelihood of subtle errors is greater than ever before. Moreover, since computerised systems are ubiquitous (e.g. planes, railways, and nuclear power plants), the impact of such errors will certainly be far-reaching. In the past such errors have resulted in a loss of time, money, and even human lives. The development of (fully-automatic) model checking technologies --- pioneered by the recent ACM Turing Award winners Clarke, Emerson, and Sifakis --- has been so influential in minimising the likelihood of subtle errors that model checking has been adopted by major companies including IBM, Intel, Motorola, and NASA. Despite its success, model checking suffers from the inherent state-explosion problem, which remains difficult today even though a substantial progress has been made in the past two decades. 

The past fifteen years have seen an increasing level of awareness amongst researchers that modelling computerised systems as infinite-state systems is not only more suitable, but might also help circumvent the notorious state-explosion problem. Such a modelling approach views the parameters that cause the state-explosion problem as potentially unbounded or infinite. These include the sizes of arrays, stacks, queues, integer or real valued variables, discrete-time or real-time clocks, and the number of processes in distributed protocols. Instead of the state-explosion problem, such abstractions as infinite-state systems yield undecidability in general. The field of infinite-state model checking aims to develop tools and techniques to deal with this problem. Broadly speaking, approaches to infinite-state model checking can be classified as follows:

1. Restrictions to decidable formalisms.

2. General (undecidable) formalisms with the aid of decidable semantic restrictions or semi-algorithms

Most research in infinite-state model checking thus far adopts only one of these approaches without seriously considering the other. Moreover, little has been done to see the connections between these two approaches. This is unfortunate since both approaches have their own disadvantages that can be considerably minimised only by considering both approaches in parallel. The project proposes a particular hybrid approach taking into account the two aforementioned approaches simultaneously. The goal is to systematically develop generic tools and techniques for infinite-state model checking aiming for both sound theoretical foundations and practical applicability. This project focuses on general formalisms that are inspired by various notions of finite-state transducers, as they are known to be clean, expressive, and most amenable to theoretical analysis.

This project is funded by EPSRC Postdoctoral Fellowship in Theoretical Computer Science.