When Simulation Meets Antichains

Parosh Abdulla, Yu-Fang Chen, Lukas Holik, Richard Mayr, Tomas Vojnar

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
EditorsJavier Esparza, Rupak Majumdar
PublisherSpringer-Verlag GmbH
Number of pages17
ISBN (Print)978-3-642-12001-5
Publication statusPublished - 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg


Dive into the research topics of 'When Simulation Meets Antichains'. Together they form a unique fingerprint.

Cite this