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). FIT-TR-2010-01, Brno: Faculty of Information Technology BUT, 2010.
Czech title
Když se simulace potká s protiřetězcem (za testováním jazykové inkluze nedeterministických konečných (stromových) automatů)
Type
technical report
Language
english
Authors
Abdulla Parosh A. (Uppsala)
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)
URL
Keywords

finite automata, tree automata, language inclusion, universality, 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 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.

Published
2010
Pages
22
Publisher
Faculty of Information Technology BUT
Place
FIT-TR-2010-01, Brno, CZ
BibTeX
@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"
}
Back to top