Tree Automata swMATH ID: 28835 Software Authors: Peter Lammich 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; Real_Impl; LTL_to_GBA; Gabow SCC; CAVA LTL Modelchecker; Presburger Automata; CAVA; CAVA Automata Library; Dijkstra Shortest Path; Fiat; Lifting; Transfer; Autoref; Locales; HOL; CSI Cited in: 3 Publications 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) Citations by Year