TAGED Approximations for Temporal Properties Model-Checking - Archive ouverte HAL Access content directly
Conference Papers Year : 2009

TAGED Approximations for Temporal Properties Model-Checking

(1) , (1, 2) , (1)
1
2

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.
Fichier principal
Vignette du fichier
rltl-hal.pdf (226.11 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00380048 , version 1 (29-04-2009)

Identifiers

  • HAL Id : inria-00380048 , version 1

Cite

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. ⟨inria-00380048⟩
110 View
125 Download

Share

Gmail Facebook Twitter LinkedIn More