Publication Details
When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (Uppsala)
Mayr Richard (UEDIN)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
finite automata, tree automata, language inclusion, universality, 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 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.
@TECHREPORT{FITPUB9152,
author = "A. Parosh Abdulla and Luk\'{a}\v{s} Hol\'{i}k and Yu-Fang Chen and Richard Mayr and Tom\'{a}\v{s} Vojnar",
title = "When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata)",
pages = 22,
year = 2010,
location = "FIT-TR-2010-01, Brno, CZ",
publisher = "Faculty of Information Technology BUT",
language = "english",
url = "https://www.fit.vut.cz/research/publication/9152"
}