Model-Checking of CTL on Infinite Kripke Structures Defined by Simple Graph Grammars

Yves-Marie Quemener 1 Thierry Jéron 1
1 PAMPA - Models and Tools for Programming Distributed Parallel Architectures
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, INRIA Rennes
Abstract : We present an algorithm for checking whether an infinite transition system, defined by a graph grammar of a restricted kind, is a model of a formula of the temporal logic CTL. We first present the syntax and the semantics of CTL, that are defined with respect to transition systems, labelled with atomic propositions. Then, we show how to adapt the formalism of graph grammars, for expressing such infinite transition systems. Our algorithm treats such a finite representation, and modify it, ensuring that the labelling for formulas remains coherent with the truth values of the different states of the infinite transition system.
Type de document :
Rapport
[Research Report] RR-2563, INRIA. 1995
Liste complète des métadonnées

https://hal.inria.fr/inria-00074118
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:33:27
Dernière modification le : mercredi 11 avril 2018 - 02:00:28
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:05:33

Fichiers

Identifiants

  • HAL Id : inria-00074118, version 1

Citation

Yves-Marie Quemener, Thierry Jéron. Model-Checking of CTL on Infinite Kripke Structures Defined by Simple Graph Grammars. [Research Report] RR-2563, INRIA. 1995. 〈inria-00074118〉

Partager

Métriques

Consultations de la notice

169

Téléchargements de fichiers

529