Reduction of Nondeterministic Tree Automata
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F16%3APU122830" target="_blank" >RIV/00216305:26230/16:PU122830 - isvavai.cz</a>
Result on the web
<a href="http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_46" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-662-49674-9_46</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-662-49674-9_46" target="_blank" >10.1007/978-3-662-49674-9_46</a>
Alternative languages
Result language
angličtina
Original language name
Reduction of Nondeterministic Tree Automata
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GJ16-24707Y" target="_blank" >GJ16-24707Y: Efficient Automata Techniques for Formal Reasoning</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Tools and Algorithms for the Construction and Analysis of Systems
ISBN
978-3-662-49673-2
ISSN
—
e-ISSN
—
Number of pages
19
Pages from-to
717-735
Publisher name
Springer Verlag
Place of publication
Berlin Heidelberg
Event location
Eindhoven, The Netherlands
Event date
Apr 2, 2016
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000406428000046