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.
finite automata, tree automata, language inclusion, universality, 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 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.
@misc{BUT192702,
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)",
year="2010",
pages="22",
publisher="Faculty of Information Technology BUT",
address="FIT-TR-2010-01, Brno",
url="http://www.fit.vutbr.cz/~holik/pub/FIT-TR-2010-001.pdf"
}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
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