Falsification-aware Semantics for CTL and Its Inconsistency-tolerant Subsystem: Towards Falsification-aware Model Checking

This study introduces two falsification-aware Kripke-style semantics for computation tree logic (CTL). The equivalences among the proposed falsification-aware Kripke-style semantics and the standard Kripke-style semantics for CTL are proven. Furthermore, a new logic, inconsistency-tolerant CTL (ICTL) is semantically defined and obtained from the proposed falsification-aware Kripke-style semantics for CTL by deleting a characteristic condition on the labeling function of the semantics. Because ICTL is regarded as an inconsistency-tolerant and many-valued logic, the proposed semantic framework for CTL and ICTL is regarded as a unified framework for combining and generalizing the standard, inconsistency-tolerant, and many-valued semantic frameworks. This unified semantic framework is useful for generalized model checking, referred to here as falsification-aware model checking.