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.