A completion algorithm for lattice tree automata

Thomas Genet (1, 2) , Tristan Le Gall (3) , Axel Legay (1, 4) , Valérie Murat (1, 2)

1 IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires
2 CELTIQUE - Software certification with semantic analysis
3 DILS - Département Ingénierie Logiciels et Systèmes
4 TRISKELL - Reliable and efficient component based software engineering

When dealing with infinite-state systems, Regular Tree Model Checking approaches may have some difficulties to represent infinite sets of data. We propose Lattice Tree Automata, an extended version of tree automata to represent complex data domains and their related operations in an efficient manner. Moreover, we introduce a new completion-based algorithm for computing the possibly infinite set of reachable states in a finite amount of time. This algorithm is independent of the lattice making it possible to seamlessly plug abstract domains into a Regular Tree Model Checking algorithm. As a first instance, we implemented a completion with an interval abstract domain. We provide some experiments showing that this implementation permits to scale up regular tree model-checking of Java programs dealing with integer arithmetics.

Keywords: Robots; Abstract domains; Completion algorithms; Extended versions; Infinite state systems; Integer arithmetic; Java program; Regular tree; Tree automata; Algorithms; Computer software; Forestry; Integer programming; Java programming language; Model checking; Trees (mathematics); Automata theory; Computer Programing; Computer Programs; Programing Languages

Domains: Computer Science [cs]

Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat. A completion algorithm for lattice tree automata. CIAA 2013 - 18th International Conference on Implementation and Application of Automata, Jul 2013, Halifax, NS, Canada. pp.134-145, ⟨10.1007/978-3-642-39274-0_13⟩. ⟨cea-01834984⟩