Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Kailiang Ji Connect in order to contact the contributor
Submitted on : Thursday, December 10, 2015 - 12:04:50 AM
Last modification on : Friday, January 21, 2022 - 3:15:30 AM
Long-term archiving on: : Saturday, April 29, 2017 - 11:09:06 AM


Files produced by the author(s)




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⟩



Record views


Files downloads