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

Citations by Year