CTL Model-Checking over Logics with Non-Classical Negations

In earlier work [9], we defined CTL model-checking over finite-valued logics with De Morgan negation. In this paper, we extend this work to logics with intuitionistic, Galois and minimal negations, calling the resulting language   CTL. We define   CTL operators and show that they can be computed using fixpoints. We further discuss how to extend our existing multi-valued model-checker   Chek [8] to reasoning over these logics.

• Type: Conference
• Year: 2003
• Where: ISMVL
• Authors: Marsha Chechik, Wendy MacCaull
• Keywords: Artificial Intelligence, CTL Model-checking, De Morgan Negation, ISMVL 2003, finite-valued Logics