When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata)

• http://www.springerlink.com/content/a2g32650q853l185/

NFA, tree-automata, universality, language inclusion, simulation, antichain

We describe a new and more efficient algorithm for checking universality and language inclusion on nondeterministic finite word automata (NFA) and tree automata (TA). To the best of our knowledge, the antichain-based approach proposed by De Wulf et al. was the most efficient one so far. Our idea is to exploit a simulation relation on the states of finite automata to accelerate the antichain-based algorithms. Normally, a simulation relation can be obtained fairly efficiently, and it can help the antichain-based approach to prune out a large portion of unnecessary search paths.We evaluate the performance of our new method on NFA/TA obtained from random regular expressions and from the intermediate steps of regular model checking. The results show that our approach significantly outperforms the previous antichain-based approach in most of the experiments.

We describe a new and more efficient algorithm for checking universality
and language inclusion on nondeterministic finite word automata (NFA)
and tree automata (TA). To the best of our knowledge, the antichain-based approachIC0901
proposed by De Wulf et al. was the most efficient one so far. Our idea is
to exploit a simulation relation on the states of finite automata to accelerate the
antichain-based algorithms. Normally, a simulation relation can be obtained fairly
efficiently, and it can help the antichain-based approach to prune out a large portion
of unnecessary search paths.We evaluate the performance of our new method
on NFA/TA obtained from random regular expressions and from the intermediate
steps of regular model checking. The results show that our approach significantly
outperforms the previous antichain-based approach in most of the experiments.