Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae

David Déharbe Anamaria Martins Moreira Christophe Ringeissen 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : A factor in the complexity of conventional algorithms for model checking Computation Tree Logic (CTL) is the size of the formulae, and, more precisely, the number of fixpoint operators. This paper addresses the following questions: given a CTL formula, is there an equivalent formula with fewer fixpoint operators? and how term rewriting techniques may be used to find it? Moreover, for some sublogics of CTL, e.g. the sub-logic NFCTL (no fixpoint computation tree logic), more efficient verification procedures are available. This paper also addresses the problem of testing whether an expression belongs or not to NFCTL, and providing support in the choice of the most efficient amongst different available verification algorithms. In this direction, we propose a rewrite system modulo AC, and discuss its implementation in ELAN, showing how this rewriting process can be plugged in a formal verification tool.
Type de document :
Communication dans un congrès
Sophie Tison. International Conference on Rewriting Techniques and Applications - RTA'2002, Jul 2002, Copenhagen, Denmark, Springer-Verlag, 2378, pp.207-221, 2002, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00100863
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:52:30
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100863, version 1

Collections

Citation

David Déharbe, Anamaria Martins Moreira, Christophe Ringeissen. Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae. Sophie Tison. International Conference on Rewriting Techniques and Applications - RTA'2002, Jul 2002, Copenhagen, Denmark, Springer-Verlag, 2378, pp.207-221, 2002, Lecture Notes in Computer Science. 〈inria-00100863〉

Partager

Métriques

Consultations de la notice

73