CTL Model Checking in Deduction Modulo

Kailiang Ji 1, *
Abstract : 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.
Type de document :
Communication dans un congrès
Automated Deduction - CADE-25, Aug 2015, Berlin, Germany. pp 295-310, 2015, 〈10.1007/978-3-319-21401-6_20〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01241132
Contributeur : Kailiang Ji <>
Soumis le : jeudi 10 décembre 2015 - 00:04:50
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : samedi 29 avril 2017 - 11:09:06

Fichier

paper_20.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

114

Téléchargements de fichiers

86