Skip to main content
Department of Information Technology

When Simulation Meets Antichains
(on Checking Language Inclusion of NFA)


Yu-Fang Chen, Academia Sinica, Taipei, Taiwan

Date and Time

Thursday, March 18th, 2010 at 13:30


Polacksbaken, room 1145


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 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



Back to the seminar page

Updated  2010-03-15 01:25:06 by Frédéric Haziza.