CTL Model-Checking Over Logics with Non-Classical Negations
Abstract
In earlier work, 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 to reasoning over these
logics.