Tree Automata
swMATH ID: | 28835 |
Software Authors: | Lammich, Peter |
Description: | Tree Automata: This work presents a machine-checked tree automata library for Standard-ML, OCaml and Haskell. The algorithms are efficient by using appropriate data structures like RB-trees. The available algorithms for non-deterministic automata include membership query, reduction, intersection, union, and emptiness check with computation of a witness for non-emptiness. The executable algorithms are derived from less-concrete, non-executable algorithms using data-refinement techniques. The concrete data structures are from the Isabelle Collections Framework. Moreover, this work contains a formalization of the class of tree-regular languages and its closure properties under set operations. |
Homepage: | https://www.isa-afp.org/entries/Tree-Automata.html |
Dependencies: | Isabelle |
Related Software: | Archive Formal Proofs; Isabelle/HOL; Light-weight Containers; CeTA; Isabelle; Dijkstra Shortest Path; Autoref; Real_Impl; LTL_to_GBA; Gabow SCC; CAVA LTL Modelchecker; Presburger Automata; CAVA; CAVA Automata Library; Fiat; Lifting; Transfer; Locales; HOL; CSI |
Cited in: | 3 Documents |
Cited by 5 Authors
2 | Lammich, Peter |
1 | Felgenhauer, Bertram |
1 | Lochbihler, Andreas |
1 | Thiemann, René |
1 | Tuerk, Thomas |
Cited in 2 Serials
1 | Information and Computation |
1 | Journal of Automated Reasoning |
Cited in 1 Field
3 | Computer science (68-XX) |