Skip to Main content Skip to Navigation
Conference papers

When Simulation Meets Antichains

Abstract : 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
Document type :
Conference papers
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Emmanuelle Grousset Connect in order to contact the contributor
Submitted on : Friday, February 26, 2010 - 4:30:43 PM
Last modification on : Wednesday, November 24, 2021 - 9:54:07 AM
Long-term archiving on: : Friday, June 18, 2010 - 8:27:56 PM


Files produced by the author(s)


  • HAL Id : inria-00460294, version 1



Parosh Aziz Abdulla, yu-Fang Chen, Lukáš Holík, Richard Mayr, Tomáš Vojnar. When Simulation Meets Antichains. TACAS'10, the 16th International Conference on Tools And Algorithms for the Construction and Analysis of Systems, Mar 2010, Paphos, Cyprus. ⟨inria-00460294⟩



Record views


Files downloads