Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications

Studia Logica 75 (1):125-157 (2003)
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 (ATL). The key insight in ATL is that the path quantifiers of CTL could be replaced by cooperation modalities, of the form , where is a set of agents. The intended interpretation of an ATL formula is that the agents can cooperate to ensure that holds (equivalently, that have a winning strategy for ). 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 (ATEL) — shares the tractability of model checking with its ATL parent, and is a succinct and expressive language for reasoning about game-like multiagent systems.
Keywords Philosophy   Logic   Mathematical Logic and Foundations   Computational Linguistics
Categories (categorize this paper)
Reprint years 2004
DOI 10.1023/A:1026185103185
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history
Request removal from index
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 27,220
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA
A Dynamic Logic of Agency I: Stit, Capabilities and Powers. [REVIEW]Andreas Herzig & Emiliano Lorini - 2010 - Journal of Logic, Language and Information 19 (1):89-121.
Reasoning with Protocols Under Imperfect Information.Eric Pacuit & Sunil Simon - 2011 - Review of Symbolic Logic 4 (3):412-444.

View all 12 citations / Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

29 ( #175,885 of 2,164,581 )

Recent downloads (6 months)

1 ( #347,948 of 2,164,581 )

How can I increase my downloads?

My notes
Sign in to use this feature

There  are no threads in this forum
Nothing in this forum yet.

Other forums