Technical report

 
Abdulla, P., A., Holík, L., Chen, Y., Mayr, R., Vojnar, T.: When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata), FIT-TR-2010-01, Brno, CZ, FIT VUT, 2010, p. 22
Publication language:english
Original title:When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata)
Title (cs):Když se simulace potká s protiřetězcem (za testováním jazykové inkluze nedeterministických konečných (stromových) automatů)
Pages:22
Place:FIT-TR-2010-01, Brno, CZ
Year:2010
Publisher:Faculty of Information Technology BUT
URL:http://www.fit.vutbr.cz/~holik/pub/FIT-TR-2010-001.pdf [PDF]
Keywords
finite automata, tree automata, language inclusion, universality, simulation, antichain
Annotation
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.
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.
BibTeX:
@TECHREPORT{
   author = {A. Parosh Abdulla and Lukáš Holík and Yu-Fang Chen and
	Richard Mayr and Tomáš 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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=9152}
}