Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and Its Applications

Studia Logica 75 (1):125-157 (2003)
  Copy   BIBTEX

Abstract

Branching-time temporal logics have proved to be an extraordinarily successful tool in the formal specification and verification of distributed systems. Much of their success stems from the tractability of the model checking problem for the branching time logic CTL, which has made it possible to implement tools that allow designers to automatically verify that systems satisfy requirements expressed in CTL. Recently, CTL was generalised by Alur, Henzinger, and Kupferman in a logic known as "Alternating-time Temporal Logic". The key insight in ATL is that the path quantifiers of CTL could be replaced by "cooperation modalities", of the form $\langle \langle \Gamma \rangle \rangle $, where Γ is a set of agents. The intended interpretation of an ATL formula $\langle \langle \Gamma \rangle \rangle \varphi $ is that the agents Γ can cooperate to ensure that φ holds. In this paper, we extend ATL with knowledge modalities, of the kind made popular in the work of Fagin, Halpern, Moses, Vardi and colleagues. Combining these knowledge modalities with ATL, it becomes possible to express such properties as "group Γ can cooperate to bring about φ iff it is common knowledge in Γ that ψ". The resulting logic -- Alternating-time Temporal Epistemic Logic -- shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems

Other Versions

original van der Hoek, Wiebe; Wooldridge, Michael (2003) "Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications". Studia Logica 75(1):125-157

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 98,072

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2011-05-29

Downloads
28 (#657,834)

6 months
6 (#736,281)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Planning-based knowing how: A unified approach.Yanjun Li & Yanjing Wang - 2021 - Artificial Intelligence 296 (C):103487.
Data-informed knowledge and strategies.Junli Jiang & Pavel Naumov - 2022 - Artificial Intelligence 309 (C):103727.

View all 18 citations / Add more citations

References found in this work

No references found.

Add more references