Tree Regular Model Checking for Lattice-Based Automata

Thomas Genet 1 Tristan Le Gall 2 Axel Legay 3 Valérie Murat 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
3 TRISKELL - Reliable and efficient component based software engineering
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Tree Regular Model Checking (TRMC) is the name of a family of techniques for analyzing infinite-state systems in which states are represented by terms, and sets of states by Tree Automata (TA). The central problem in TRMC is to decide whether a set of bad states is reachable. The problem of computing a TA representing (an over-approximation of) the set of reachable states is undecidable, but efficient solutions based on completion or iteration of tree transducers exist. Unfortunately, the TRMC framework is unable to efficiently capture both the complex structure of a system and of some of its features. As an example, for JAVA programs, the structure of a term is mainly exploited to capture the structure of a state of the system. On the counter part, integers of the java programs have to be encoded with Peano numbers, which means that any algebraic operation is potentially represented by thousands of applications of rewriting rules. In this paper, we propose Lattice Tree Automata (LTAs), an extended version of tree automata whose leaves are equipped with lattices. LTAs allow us to represent possibly infinite sets of interpreted terms. Such terms are capable to represent complex domains and related operations in an efficient manner. We also extend classical Boolean operations to LTAs. Finally, as a major contribution, we introduce a new completion-based algorithm for computing the possibly infinite set of reachable interpreted terms in a finite amount of time.
Type de document :
Communication dans un congrès
CIAA - 18th International Conference on Implementation and Application of Automata, Jul 2013, Halifax, Canada. Springer, 7982, 2013, LNCS
Liste complète des métadonnées

https://hal.inria.fr/hal-00924849
Contributeur : Thomas Genet <>
Soumis le : mardi 7 janvier 2014 - 11:24:51
Dernière modification le : jeudi 9 février 2017 - 16:05:34

Identifiants

  • HAL Id : hal-00924849, version 1

Citation

Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat. Tree Regular Model Checking for Lattice-Based Automata. CIAA - 18th International Conference on Implementation and Application of Automata, Jul 2013, Halifax, Canada. Springer, 7982, 2013, LNCS. <hal-00924849>

Partager

Métriques

Consultations de la notice

494