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.