Relational Version of the Multi-agent Computation Tree Logic $\mathcal{CTLK}$ - S. I. Bashmakov; K. A. Smelykh (Известия Иркутского государственного университета: Серия "Математика", 2024)
This paper deals with multi-agent computation tree logic --- $\mathcal{CTLK}$ (Computation Tree Logic with Knowledge). Each agent represents its own computational route of the initial problem, and new branches of possible computational routes spawn new agents. The logic $\mathcal{CTLK}$ is a natural enrichment of $\mathcal{CTL}$ by new knowledge operators. We introduce alternative to automata Kripke's relational semantics, describes properties of $\mathcal{CTLK}^{Rel}$-frame and proves finite approximability.