Changing Observations in Epistemic Temporal Logic

TL;DR

This paper introduces a new operator in epistemic temporal logic that models changing observational powers of agents, extending CTL*K's expressivity and providing a decision procedure for model-checking.

Contribution

It extends CTL*K with an operator for changing observations, increasing expressivity and offering a more efficient model-checking procedure.

Findings

The new operator strictly increases logic expressivity.

Model-checking reduces to CTL*K, ensuring decidability.

A direct decision procedure with improved complexity is provided.

Abstract

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 perfect-recall agents to account for changes of observation, and we show that this new operator strictly 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 its complexity is not optimal. Indeed we provide a direct decision procedure with better complexity.