Temporal Logics for Multi-Agent Systems

Temporal logic formalizes reasoning about the possible behaviours of a system over time. For example, a temporal formula may stipulate that an occurrence of event A may be, or must be, followed by an occurrence of event B. Traditional temporal logics, however, are insufficient for reasoning about multi-agent systems. In order to stipulate, for example, that a specific agent can ensure that A is followed by B, references to agents, their capabilities, and their intentions must be added to the logic, yielding Alternating-time Temporal Logic (ATL) [1]. ATL is a temporal logic that is interpreted over multi-player games, whose players correspond to agents that pursue temporal objectives. The hardness of the model-checking problem – whether a given formula is true for a given multi-agent system – depends on how the players decide on the next move in the game (for example, whether they take turns, or make independent concurrent decisions, or bid for the next move), how the outcome of a move is computed (deterministically or stochastically), how much memory the players have available for making decisions, and which kind of objectives they pursue (qualitative or quantitative). The expressiveness of ATL is still insufficient for reasoning about equilibria and related phenomena in non-zero-sum games, where the players may have interfering but not necessarily complementary objectives. For this purpose, the behavioural strategies (a. k. a. policies) of individual players can been added to the logic as quantifiable first-order entities, yielding Strategy Logic [2]. We survey several known results about these multi-player game logics and point out some open problems.

Authors

• Thomas A. Henzinger Institute of Science and Technology Austria

Keywords

• logics of agency
• temporal logic
• ATL