Detail publikace

Reduction of Nondeterministic Tree Automata

HOLÍK, L. ALMEIDA, R. MAYR, R.

Originální název

Reduction of Nondeterministic Tree Automata

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

We present an efficient algorithm to reduce the size of nondeterministic tree automata, while retaining their language. It is based on new transition pruning techniques, and quotienting of the state space w.r.t. suitable equivalences. It uses criteria based on combinations of downward and upward simulation preorder on trees, and the more general downward and upward language inclusions. Since tree-language inclusion is EXPTIME-complete, we describe methods to compute good approximations in polynomial time. We implemented our algorithm as a module of the well-known libvata tree automata library, and tested its performance on a given collection of tree automata from various applications of libvatain regular model checking and shape analysis, as well as on various classes of randomly generated tree automata. Our algorithm yields substantially smaller and sparser automata than all previously known reduction techniques, and it is still fast enough to handle large instances.

Klíčová slova

tree automata, reduction, simulation, lookahead simulation forward simulation, backward simulation

Autoři

HOLÍK, L.; ALMEIDA, R.; MAYR, R.

Vydáno

16. 5. 2016

Nakladatel

Springer Verlag

Místo

Berlin Heidelberg

ISBN

978-3-662-49673-2

Kniha

Tools and Algorithms for the Construction and Analysis of Systems

Edice

Volume 9636 of the series Lecture Notes in Computer Science

Strany od

717

Strany do

735

Strany počet

19

URL

http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_46

BibTex

@inproceedings{BUT133495,
  author="Lukáš {Holík} and Ricardo {Almeida} and Richard {Mayr}",
  title="Reduction of Nondeterministic Tree Automata",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2016",
  series="Volume 9636 of the series Lecture Notes in Computer Science",
  pages="717--735",
  publisher="Springer Verlag",
  address="Berlin Heidelberg",
  doi="10.1007/978-3-662-49674-9\{_}46",
  isbn="978-3-662-49673-2",
  url="http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_46"
}