Personal tools
You are here: Home Events Richard Mayr

Richard Mayr

Title: Solving PSPACE-complete problems in automata theory

Abstract:

Finite automata are a fundamental building block in formal software
verification, databases, learning theory and many other areas of computer
science. However, central automata problems like language inclusion, equality and
universality are computationally hard (PSPACE-complete) and so far only very tiny instances
could be solved.
Analogously to the progress in SAT-solvers (for the class NP),
PSPACE-hardness is no longer an excuse for not solving these problems.
This talk gives an introduction to recent work on solving
universality/inclusion problems for finite automata and Buchi-automata.
The main techniques are based on subsumption relations between (sets of)
states, which rely on several variants of simulation preorder.
These new algorithms have been implemented, and a tool demo will be given.

(A technical talk, focusing on algorithms and datastructures, will be given
in the Algorithms and Complexity Reading Group (ACRG) on Wednesday 23. Feb.)

References:

Parosh Aziz Abdulla, Yu-Fang Chen, Lorenzo Clemente, Lukas Holik, Chih Duo Hong, Richard Mayr and Tomas Vojnar. Simulation Subsumption in Ramsey-based Büchi Automata Universality and Inclusion Testing. Proc. of CAV 2010. 22nd International Conference on Computer Aided Verification. Edinburgh, UK. Volume 6174 in LNCS. 2010.

Parosh Aziz Abdulla, Yu-Fang Chen, Lukas Holik, Richard Mayr and Tomas
Vojnar. When Simulation Meets Antichains (On Checking Language Inclusion of
Nondeterministic Finite (Tree) Automata). Proc. of TACAS 2010, Sixteenth
International Conference on Tools and Algorithms for the Construction and
Analysis of Systems. Paphos, Cyprus. Volume 6015 in LNCS. 2010.
(EATCS Best Theory Paper Award, 2010.)

Document Actions