Detail publikace

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

Originální název

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

Anglický název

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

Jazyk

en

Originální abstrakt

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.

Anglický abstrakt

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.

BibTex


@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)",
  annote="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.",
  address="Springer Verlag",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  chapter="34731",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  year="2010",
  month="march",
  pages="158--174",
  publisher="Springer Verlag",
  type="conference paper"
}