Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
Studia Logica 75 (1) (2003)
| 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 | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,701 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesNatasha Alechina, Brian Logan, Hoang Nga Nguyen & Abdur Rakib (2009). Verifying Time, Memory and Communication Bounds in Systems of Reasoning Agents. Synthese 169 (2):385 - 403.
Ron van der Meyden & Ka-shu Wong (2003). Complete Axiomatizations for Reasoning About Knowledge and Branching Time. Studia Logica 75 (1):93 - 123.
Andreas Herzig & Emiliano Lorini (2010). A Dynamic Logic of Agency I: Stit, Capabilities and Powers. Journal of Logic, Language and Information 19 (1).
Thomas Ågotnes & Dirk Walther (2009). A Logic of Strategic Ability Under Bounded Memory. Journal of Logic, Language and Information 18 (1).
Wiebe van Der Hoek, Mark Roberts & Michael Wooldridge (2007). Social Laws in Alternating Time: Effectiveness, Feasibility, and Synthesis. Synthese 156 (1):1 - 19.
Wiebe van der Hoek, Mark Roberts & Michael Wooldridge (2007). Social Laws in Alternating Time: Effectiveness, Feasibility, and Synthesis. Synthese 156 (1).
M. Kacprzak & W. Penczek (2004). A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic. Synthese 142 (2):203 - 227.
Valentin Goranko & Wojciech Jamroga (2004). Comparing Semantics of Logics for Multi-Agent Systems. Synthese 139 (2):241 - 280.
Thomas Ågotnes (2006). Action and Knowledge in Alternating-Time Temporal Logic. Synthese 149 (2):375 - 407.
Analytics
Monthly downloads |
Added to index2009-01-28Total downloads13 ( #87,971 of 549,122 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
