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
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
3 DILS - Département Ingénierie Logiciels et Systèmes
4 TRISKELL - Reliable and efficient component based software engineering
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
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 : Tree automata Algorithms Computer software Forestry Integer programming Java programming language Model checking Trees (mathematics) Automata theory Computer Programing Computer Programs Programing Languages Robots Regular tree Java program Integer arithmetic Infinite state systems Extended versions Completion algorithms Abstract domains
Document type :
Conference papers
Complete list of metadatas
https://hal-cea.archives-ouvertes.fr/cea-01834984
Contributor : Léna Le Roy <>
Submitted on : Wednesday, July 11, 2018 - 10:02:34 AM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Links full text

istex

Identifiers

Collections

CEA | CNRS | UNIV-RENNES1 | DRT | IRISA | INRIA | LIST | UR1-UFR-ISTIC | UNIV-RENNES | INSTITUT-TELECOM | INSA-GROUPE | IRISA-D4

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

368

Contact

CCSD