Defining and Model-Checking an Epistemic Temporal Logic with Changes of Observations

We define a logic for systems with imperfect information, CTL∗K∆. It inherits operators from temporal and epistemic logics, as well as a new one that allows agents to dynamically change their observation of the system. We first define it for single-agent settings with synchronous perfect recall. We define an equivalent semantics, that is used later for model-checking the logic, and proved to be equivalent. We give an algorithm for model-checking. Finally, we extend our logic to multi-agent settings.