Publication result detail

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

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y.; MAYR, R.

Original Title

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

English Title

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

Type

Paper in proceedings outside WoS and Scopus

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

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

Keywords

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

Key words in English

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

Authors

HOLÍK, L.; VOJNAR, T.; ABDULLA, P.; CHEN, Y.; MAYR, R.

RIV year

2012

Released

30.03.2010

Publisher

Springer Verlag

Location

Berlín

ISBN

978-3-642-12001-5

Book

Tools and Algorithms for the Construction and Analysis of Systems

Edition

Lecture Notes in Computer Science

Volume

6015

Pages from

158

Pages to

174

Pages count

17

URL

http://www.springerlink.com/content/a2g32650q853l185/

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)",
  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/"
}