Tenth and final Meeting
- Axel Legay (Liège)
-
Title: Iterating Transducers: Theory and Practice (Slides)
- Abstract:
``Regular model checking'' is the name of a family of techniques for
analyzing infinite-state systems, in which states are represented by
finite or infinite words, 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. In this context, the central
problem is to compute the iterative closure of a finite-state
transducer. In this work, we investigate the possibilities of applying
generic techniques in cases where only specific techniques have been
exploited so far. Finding that existing generic techniques are often not
applicable in cases easily handled by specific techniques (systems with
integers, with reals, ...), we have developed new approaches to
iterating transducers. These approaches build on earlier work, but
exploit a number of new conceptual and algorithmic ideas, often induced
with the help of experiments, that give it a broad scope, as well as
good performance.