We study dynamic changes of agents' observational power in logics of knowledge and time We consider CTL'K, the extension of CTLwith 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 CTLK, 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-chocking procedure with better complexity. © 2019 International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org) Ail rights reserved.
Reasoning about changes of observational power in logics of knowledge and time / Barriere, A.; Maubert, B.; Murano, A.; Rubin, S.. - 2:(2019), pp. 971-979. (Intervento presentato al convegno 18th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2019).
Reasoning about changes of observational power in logics of knowledge and time
Maubert, B.;Murano, A.;Rubin, S.
2019
Abstract
We study dynamic changes of agents' observational power in logics of knowledge and time We consider CTL'K, the extension of CTLwith 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 CTLK, 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-chocking procedure with better complexity. © 2019 International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org) Ail rights reserved.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
