Tree-like Model Structure for the Branching-Time Temporal Logic of Knowledge

Computation Tree Logic (CTL) serves as a means to specify systems un dergoing temporal changes, incorporating quantification across potential future scenarios. Sometimes systems not only evolve over time but also encompass informational aspects. We introduce a temporal logic of knowledge (CTL-K) amalgamating CTL and epistemic logic S5. Despite the existence of some tem poral logics of knowledge, CTL-K allows us to leverage CTL’s advantages over LTL. Notably, we propose a tree-like model structure for the semantics of CTL K, whose temporal part of model is a set of trees. This model structure can be utilized in theorem proving methods such as resolution-based methods in order to make it easier to prove the correctness of their calculus steps, especially to prove satisfiability preservation. We show that a CTL-K formula is satisfiable iff it is satisfiable in a tree-like model structure.