Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 2:52:30 PM
Last modification on : Friday, February 26, 2021 - 3:28:05 PM


  • HAL Id : inria-00100863, version 1



David Déharbe, Anamaria Martins Moreira, Christophe Ringeissen. Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae. International Conference on Rewriting Techniques and Applications - RTA'2002, Thomas Arts, Jul 2002, Copenhagen, Denmark, pp.207-221. ⟨inria-00100863⟩



Record views