TAGED Approximations for Temporal Properties Model-Checking

Roméo Courbis 1 Pierre-Cyrille Heam 1, 2 Olga Kouchnarenko 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Reachability analysis turned out to be a very efficient verification technique for proving security properties on infinite state systems modeled by term rewriting systems (TRSs). Unfortunately, the reachability problem is in general undecidable on non terminating TRSs. Rewriting over-approximations of (a set of) reachable terms allow semi-deciding this problem by showing that undesirable terms modeling insecurity property do not belong to these approximations. In this paper, we propose to exploit rewriting approximations for model-checking of linear time temporal properties. We show the helpfulness of the reachability analysis for model-checking three useful temporal property patterns on infinite state rewriting graphs. The reachability problem being in general undecidable on non terminating TRSs, we provide a construction based on tree automata with global equalities and disequalities (TAGED for short), and then design approximation-based semi-decision procedures to model-check useful temporal patterns on infinite state rewriting graphs. To show that the above TAGED-based construction can be effectively carried out, complexity analysis for rewriting TAGED-definable languages is given. A deep integration of our proposals in the model-checking process is achieved by using the same over-approximations for computing (finite representations of) some parts of the infinite state model, as for verifying linear time temporal properties.
Type de document :
Communication dans un congrès
Proceedings of the 14th International Conference on Implementation and Application of Automata - CIAA'09, Jul 2009, Sydney, Australia. 2009
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00380048
Contributeur : Olga Kouchnarenko <>
Soumis le : mercredi 29 avril 2009 - 16:58:16
Dernière modification le : jeudi 15 février 2018 - 08:48:09
Document(s) archivé(s) le : lundi 15 octobre 2012 - 09:45:51

Fichier

rltl-hal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00380048, version 1

Citation

Roméo Courbis, Pierre-Cyrille Heam, Olga Kouchnarenko. TAGED Approximations for Temporal Properties Model-Checking. Proceedings of the 14th International Conference on Implementation and Application of Automata - CIAA'09, Jul 2009, Sydney, Australia. 2009. 〈inria-00380048〉

Partager

Métriques

Consultations de la notice

212

Téléchargements de fichiers

96