Automata Minimization and Language Inclusion Checking
Speaker
Date and Time
Thursday, February 21st, 2013 at 10:30.
Location
Polacksbacken, room 1146
Abstract
Checking language inclusion of nondeterministic Buchi word automata
is PSPACE-complete, and so are related problems like language equivalence
and language universality.
While many algorithms exist (Rank, Ramsey, Safra, Piterman, Slice) they can
only handle very small instances.
We present a different approach based on automata minimization, i.e.,
finding smaller automata with the same language (see our POPL 2013 paper).
The minimization uses quotienting and transition pruning techniques,
using the semantic relations of trace-inclusion (and multipebble simulation).
Since these relations are themselves PSPACE-complete, we describe efficient
algorithms to compute good under-approximations of them.
These methods minimize automata substantially better than previous techniques
and help to solve language inclusion problems for much larger instances.
An implementation of the tools is available at www.languageinclusion.org
References
Lorenzo Clemente and Richard Mayr: Advanced Automata Minimization, POPL 2013.