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 XCTL. We define XCTL operators and show that they can be computed using fixpoints. We further discuss how to extend our existing multi-valued model-checker XChek [8] to reasoning over these logics.