Abstract: This talk introduces an automata-based approach for the verification of infinite-state systems.

In the first part of the talk, we present "regular model checking" that is a framework in which states are represented by (in)finite words, and sets of states by finite automata on these objects, and transitions by finite automata operating on pairs of state encodings, i.e. finite-state transducers. We also show how various classes of infinite-state systems can be encoded in the regular model checking framework.

In the second part of the talk, we present the automata-based techniques we developed for computing a finite representation of the transitive closure of a transducer. Such an object can be used to compute an infinite set of state in a finite time.

Finally, various extensions and results are discussed.

Axel Legay was born in 1980, Verviers, Belgium. In 2002 he obtained his diploma in computer science from the University of Liè and became a member of Pierre Wolper's team. In 2003, he obtained a master in computer sciences and entered in the Ph.D. program of the University of Liège. Legay will defend his Thesis in December 2007 and then become a Postdoc at Carnegie Mellon. Axel Legay's main research interests include verification methods for reactive and concurrent programs based on an automata-theory approach. Appointments: dcm@cs.cmu.edu