Publication Details

When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata)

ABDULLA Parosh A., HOLÍK Lukáš, CHEN Yu-Fang, MAYR Richard and VOJNAR Tomáš. When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata). In: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 6015. Berlín: Springer Verlag, 2010, pp. 158-174. ISBN 978-3-642-12001-5.
Czech title
Když se simulace setká s protiřetězcem (Za efektivním testováním jazykové inkluze nedeterministických konečných (stromových) automatů)
Type
conference paper
Language
english
Authors
Abdulla Parosh A. (Uppsala)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Mayr Richard (UEDIN)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

NFA, tree-automata, universality, language inclusion, simulation, antichain

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.

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

Published
2010
Pages
158-174
Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science
Volume
6015
Conference
European Joint Conferences on Theory and Practice of Software -- ETAPS 2010, Paphos, CY
ISBN
978-3-642-12001-5
Publisher
Springer Verlag
Place
Berlín, DE
BibTeX 
@INPROCEEDINGS{FITPUB9190,
   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 = "158--174",
   booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
   series = "Lecture Notes in Computer Science",
   volume = 6015,
   year = 2010,
   location = "Berl\'{i}n, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-12001-5",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9190"
}
Back to top