Paper Info
Title
Alternating-time dynamic logic
Abstract
We propose Alternating-time Dynamic Logic (ADL) as a multi-agent variant of Dynamic Logic in which atomic programs are replaced by coalitions. In ADL, the Dynamic Logic operators are parametrised with regular expressions over coalitions and tests. Such regular expressions describe the dynamic structure of a coalition. This means that, when moving from Dynamic Logic to ADL, the focus shifts away from describing what is executed and when, toward describing who is acting and when. While Dynamic Logic provides for reasoning about complex programs, ADL facilitates reasoning about coalitions with an inner dynamic structure, so-called coordinated coalitions. The semantics for such coalitions involves partial strategies and a variety of ways to combine them. Different combinations of partial strategies give rise to different semantics for ADL. In this paper, we mainly focus on one version of the semantics but we provide a discussion on other semantic variants of ADL together with possible syntactic extensions. We see ADL to be suitable for the specification and the verification of scheduling and planning systems, and we therefore present a model checking algorithm for ADL and investigate its computational complexity.
Year
DOI
Venue
2010
10.1145/1838206.1838273
Autonomous Agents & Multiagent Systems/Agent Theories, Architectures, and Languages
Keywords
Field
DocType
different semantics,alternating-time dynamic logic,dynamic logic operator,partial strategy,dynamic structure,focus shift,adl facilitates reasoning,regular expression,dynamic logic,different combination,model checking
Regular expression,Model checking,Scheduling (computing),Computer science,Theoretical computer science,Operator (computer programming),Dynamic logic (digital electronics),Syntax,Semantics,Computational complexity theory
Conference
Citations 
PageRank 
References 
1
0.35
8
Authors
2
Name
Order
Citations
PageRank
Nicolas Troquard126629.54
Dirk Walther210.35