Reduction of nondeterministic tree automata
From MaRDI portal
Publication:2272933
DOI10.1007/978-3-662-49674-9_46zbMATH Open1420.68105arXiv1512.08823OpenAlexW2200478861MaRDI QIDQ2272933FDOQ2272933
Authors: Ricardo Almeida, Lukáš Holik, Richard M. Mayr 
Publication date: 17 September 2019
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 libvata in 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.
Full work available at URL: https://arxiv.org/abs/1512.08823
Recommendations
- Computing Simulations over Tree Automata
- VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- A uniform (bi-)simulation-based framework for reducing tree automata
- Composed Bisimulation for Tree Automata
Cited In (13)
- TREE AUTOMATA BASED ON COMPLETE RESIDUATED LATTICE-VALUED LOGIC: REDUCTION ALGORITHM AND DECISION PROBLEMS
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- Efficient evaluation of nondeterministic automata using factorization forests
- On size reduction techniques for multitape automata
- Title not available (Why is that?)
- \(Ntyft/ntyxt\) rules reduce to \(n\)tree rules
- A uniform (bi-)simulation-based framework for reducing tree automata
- Title not available (Why is that?)
- A congruence-based perspective on finite tree automata
- Title not available (Why is that?)
- Implementation and Application of Automata
- Computing Simulations over Tree Automata
- Minimization of visibly pushdown automata using partial Max-SAT
This page was built for publication: Reduction of nondeterministic tree automata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2272933)
