Changing Observations in Epistemic Temporal Logic.

We study dynamic changes of agents' observational power in logics of knowledge and time. We consider CTL*K, the extension of CTL* with knowledge operators, and enrich it with a new operator that models a change in an agent's way of observing the system. We extend the classic semantics of knowledge for agents with perfect recall to account for changes of observation, and we show that this new operator strictly increases the expressivity of CTL* K. We also provide a model-hecking procedure for the logic we introduce, which has the same complexity as the best known model-checking procedure for the less expressive logic CTL* K.