Studia Logica 75 (1):125-157 (2003)
Authors |
|
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 (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 |
Options |
![]() ![]() ![]() ![]() |
Download options
References found in this work BETA
No references found.
Citations of this work BETA
Quantified Temporal Alethic Boulesic Doxastic Logic.Daniel Rönnedal - 2021 - Logica Universalis 15 (1):1-65.
Deontic Epistemic Stit Logic Distinguishing Modes of Mens Rea.Jan Broersen - 2011 - Journal of Applied Logic 9 (2):137-152.
Planning-Based Knowing How: A Unified Approach.Yanjun Li & Yanjing Wang - 2021 - Artificial Intelligence 296:103487.
View all 36 citations / Add more citations
Similar books and articles
Comparing Semantics of Logics for Multi-Agent Systems.Valentin Goranko & Wojciech Jamroga - 2004 - Synthese 139 (2):241 - 280.
Social Laws in Alternating Time: Effectiveness, Feasibility, and Synthesis.Wiebe van der Hoek, Mark Roberts & Michael Wooldridge - 2007 - Synthese 156 (1):1-19.
A Logic of Strategic Ability Under Bounded Memory.Thomas Ågotnes & Dirk Walther - 2009 - Journal of Logic, Language and Information 18 (1):55-77.
A Dynamic Logic of Agency I: Stit, Capabilities and Powers.Andreas Herzig & Emiliano Lorini - 2010 - Journal of Logic, Language and Information 19 (1):89-121.
Complete Axiomatizations for Reasoning About Knowledge and Branching Time.Ron van der Meyden & Ka-shu Wong - 2003 - Studia Logica 75 (1):93 - 123.
Cooperation, Knowledge, and Time: Alternating-Time Temporal Epistemic Logic and Its Applications.Wiebe van Der Hoek & Michael Wooldridge - 2003 - Studia Logica 75 (1):125-157.
Analytics
Added to PP index
2009-01-28
Total views
64 ( #180,477 of 2,519,514 )
Recent downloads (6 months)
2 ( #271,332 of 2,519,514 )
2009-01-28
Total views
64 ( #180,477 of 2,519,514 )
Recent downloads (6 months)
2 ( #271,332 of 2,519,514 )
How can I increase my downloads?
Downloads