Reasoning about strategies under partial observability and fairness constraints

Simon Busard
UC Louvain
Friday, 29 November, 2013 - 16:00
NO Solvay (5th floor)

Alternating-time Temporal Logic (ATL) is a logic to reason about strategies that a set of agents can adopt to achieve a specified collective goal. ATL can also be used to specify what agents can do in open systems, where they can interact with their environment in many different ways.
A number of extensions for this logic exist; some of them mix strategies and partial observability, some others include fairness constraints, but no work provides a unified framework for strategies, partial observability and fairness constraints. Integration of these three concepts is of particular importance when reasoning about the capabilities of agents that do not have full knowledge of a system, for instance when the agents can assume that the environment behaves in a fair way.
In this talk we present ATLK_irF , a logic combining strategies under partial observability and epistemic properties of agents in a system with fairness constraints on states. We introduce a model-checking algorithm for ATLK_irF by extending the algorithm for a full-observability variant of the logic.