Skip to Main content Skip to Navigation
Conference papers

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 (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Complete list of metadata

Cited literature [32 references]  Display  Hide  Download
Contributor : Olga Kouchnarenko Connect in order to contact the contributor
Submitted on : Wednesday, April 29, 2009 - 4:58:16 PM
Last modification on : Saturday, October 16, 2021 - 11:26:06 AM
Long-term archiving on: : Monday, October 15, 2012 - 9:45:51 AM


Files produced by the author(s)


  • HAL Id : inria-00380048, version 1


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⟩



Record views


Files downloads