Skip to main content
Department of Information Technology

Automata Minimization and Language Inclusion Checking


Date and Time

Thursday, February 21st, 2013 at 10:30.


Polacksbacken, room 1146


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


Lorenzo Clemente and Richard Mayr: Advanced Automata Minimization, POPL 2013.

Updated  2013-02-01 12:55:21 by Frédéric Haziza.