# 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.