Reduction of Nondeterministic Tree Automata

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Reduction of Nondeterministic Tree Automata

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Reduction of Nondeterministic Tree Automata

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GJ16-24707Y" target="_blank" >GJ16-24707Y: Efektivní techniky pro práci s automaty ve formálním usuzování</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Tools and Algorithms for the Construction and Analysis of Systems

ISBN

978-3-662-49673-2

ISSN

—

e-ISSN

—

Počet stran výsledku

19

Strana od-do

717-735

Název nakladatele

Springer Verlag

Místo vydání

Berlin Heidelberg

Místo konání akce

Eindhoven, The Netherlands

Datum konání akce

2. 4. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000406428000046