Publication Details

Reduction of Nondeterministic Tree Automata

ALMEIDA Ricardo, HOLÍK Lukáš and MAYR Richard. Reduction of Nondeterministic Tree Automata. In: Tools and Algorithms for the Construction and Analysis of Systems. Volume 9636 of the series Lecture Notes in Computer Science. Berlin Heidelberg: Springer Verlag, 2016, pp. 717-735. ISBN 978-3-662-49673-2. Available from: http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_46
Czech title
Redukce nedeterministických stromových automatů
Type
conference paper
Language
english
Authors
Almeida Ricardo (UEDIN)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Mayr Richard (UEDIN)
URL
Keywords

tree automata,
reduction,

simulation,
lookahead simulation
forward simulation,
backward simulation

Abstract

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.

Annotation

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.

Published
2016
Pages
717-735
Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
Series
Volume 9636 of the series Lecture Notes in Computer Science
Conference
22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Eindhoven, The Netherlands, CZ
ISBN
978-3-662-49673-2
Publisher
Springer Verlag
Place
Berlin Heidelberg, DE
DOI
UT WoS
000406428000046
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11178,
   author = "Ricardo Almeida and Luk\'{a}\v{s} Hol\'{i}k and Richard Mayr",
   title = "Reduction of Nondeterministic Tree Automata",
   pages = "717--735",
   booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
   series = "Volume 9636 of the series Lecture Notes in Computer Science",
   year = 2016,
   location = "Berlin Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-662-49673-2",
   doi = "10.1007/978-3-662-49674-9\_46",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11178"
}
Back to top