Conference paper

 
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), In: Tools and Algorithms for the Construction and Analysis of Systems, Berlín, DE, Springer, 2010, p. 158-174, ISBN 978-3-642-12001-5
Publication language:english
Original title:When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata)
Title (cs):Když se simulace setká s protiřetězcem (Za efektivním testováním jazykové inkluze nedeterministických konečných (stromových) automatů)
Pages:158-174
Proceedings:Tools and Algorithms for the Construction and Analysis of Systems
Conference:European Joint Conferences on Theory and Practice of Software -- ETAPS 2010
Series:LNCS 6015
Place:Berlín, DE
Year:2010
ISBN:978-3-642-12001-5
Publisher:Springer Verlag
URL:http://www.springerlink.com/content/a2g32650q853l185/ [PDF]
Keywords
NFA, tree-automata, universality, language inclusion, 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 approachIC0901
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:
@INPROCEEDINGS{
   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 = {158--174},
   booktitle = {Tools and Algorithms for the Construction and Analysis of
	Systems},
   series = {LNCS 6015},
   year = {2010},
   location = {Berlín, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-642-12001-5},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9190}
}