## Antichains:
A New Algorithm for Checking Universality of Finite Automata

*Martin De Wulf, Laurent Doyen,
Thomas A. Henzinger,
and Jean-Francois Raskin*

We propose and evaluate a new algorithm for checking the universality
of nondeterministic finite automata. In contrast to the standard
algorithm, which uses the subset construction to explicitly
determinize the automaton, we keep the determinization step implicit.
Our algorithm computes the least fixed point of a monotone function on
the lattice of antichains of state sets. We evaluate the performance
of our algorithm experimentally using the random automaton model
recently proposed by Tabakov and Vardi. We show that on the difficult
instances of this probabilistic model, the antichain algorithm
outperforms the standard one by several orders of magnitude. We also
show how variations of the antichain method can be used for solving
the language-inclusion problem for nondeterministic finite automata,
and the emptiness problem for alternating finite automata.

*Proceedings of the
18th International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 4144,
Springer, 2006, pp. 17-30.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2006 Springer.