CTL Model Checking in Deduction Modulo - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

CTL Model Checking in Deduction Modulo

Résumé

In this paper we give an overview of proof-search method for CTL model checking based on Deduction Modulo. Deduction Modulo is a reformulation of Predicate Logic where some axioms—possibly all—are replaced by rewrite rules. The focus of this paper is to give an encoding of temporal properties expressed in CTL, by translating the logical equivalence between temporal operators into rewrite rules. This way, the proof-search algorithms designed for Deduction Modulo, such as Resolution Modulo or Tableaux Modulo, can be used in verifying temporal properties of finite transition systems. An experimental evaluation using Resolution Modulo is presented.
Fichier principal
Vignette du fichier
paper_20.pdf (531.8 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01241132 , version 1 (10-12-2015)

Identifiants

Citer

Kailiang Ji. CTL Model Checking in Deduction Modulo. Automated Deduction - CADE-25, Aug 2015, Berlin, Germany. pp 295-310, ⟨10.1007/978-3-319-21401-6_20⟩. ⟨hal-01241132⟩

Collections

INRIA INRIA2
96 Consultations
155 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More