Reasoning about Changes of Observational Power in Logics of Knowledge and Time

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 observational power, and we show that this new operator increases the expressivity of CTL * K. We reduce the model-checking problem for our logic to that for CTL * K, which is known to be decidable. This provides a solution to the model-checking problem for our logic, but it is not optimal, and we provide a direct model-checking procedure with better complexity.