 |
Conference papers
A completion algorithm for lattice tree automata
Abstract : 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
https://hal-cea.archives-ouvertes.fr/cea-01834984
Contributor : Léna Le Roy Connect in order to contact the contributor
Submitted on : Wednesday, July 11, 2018 - 10:02:34 AM
Last modification on : Saturday, August 6, 2022 - 3:32:44 AM
Contributor : Léna Le Roy Connect in order to contact the contributor
Submitted on : Wednesday, July 11, 2018 - 10:02:34 AM
Last modification on : Saturday, August 6, 2022 - 3:32:44 AM
Links full text
