Result Details
When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Abdulla Parosh
Chen Yu-Fang
Mayr Richard
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.
NFA, tree-automata, universality, language inclusion, 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 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.
@inproceedings{BUT34731,
author="Lukáš {Holík} and Tomáš {Vojnar} and Parosh {Abdulla} and Yu-Fang {Chen} and Richard {Mayr}",
title="When Simulation Meets Antichains (On Checking Language Inclusion of Nondeterministic Finite (Tree) Automata)",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2010",
series="Lecture Notes in Computer Science",
volume="6015",
pages="158--174",
publisher="Springer Verlag",
address="Berlín",
isbn="978-3-642-12001-5",
url="http://www.springerlink.com/content/a2g32650q853l185/"
}Mathematical and Engineering Approaches to Developing Reliable and Secure Concurrent and Distributed Computer Systems, GACR, Doktorské granty, GD102/09/H042, start: 2009-01-30, end: 2012-12-31, completed
Secured, reliable and adaptive computer systems, BUT, Vnitřní projekty VUT, FIT-S-10-1, start: 2010-03-01, end: 2010-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, start: 2010-01-01, end: 2013-12-31, running