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.
|Title of host publication||Tools and Algorithms for the Construction and Analysis of Systems|
|Editors||Javier Esparza, Rupak Majumdar|
|Number of pages||17|
|Publication status||Published - 2010|
|Name||Lecture Notes in Computer Science|
|Publisher||Springer Berlin / Heidelberg|