Title
Model-Checking iterated games
Abstract
We propose a logic for the definition of the collaborative power of groups of agents to enforce different temporal objectives. The resulting temporal cooperation logic (TCL) extends ATL by allowing for successive definition of strategies for agents and agencies. Different to previous logics with similar aims, our extension cuts a fine line between extending the power and maintaining a low complexity: model-checking TCL sentences is EXPTIME complete in the logic, and fixed parameter tractable for specifications of bounded size. This advancement over non-elementary logics is bought by disallowing a too close entanglement between cooperation and competition. We show how allowing such an entanglement immediately leads to a non-elementary complexity. We have implemented a model-checker for the logic and shown the feasibility of model-checking on a few benchmarks.
Year
DOI
Venue
2013
10.1007/s00236-016-0277-y
Acta Inf.
Keywords
Field
DocType
different temporal objective,temporal cooperation logic,non-elementary logic,iterated game,low complexity,close entanglement,collaborative power,successive definition,previous logic,non-elementary complexity,model-checking tcl sentence
Model checking,EXPTIME,Quantum entanglement,Computer science,Theoretical computer science,Temporal logic,Iterated function,Bounded function
Conference
Volume
Issue
ISSN
54
7
1432-0525
Citations 
PageRank 
References 
4
0.43
21
Authors
3
Name
Order
Citations
PageRank
Chung-Hao Huang1857.55
Sven Schewe249642.54
Farn Wang31278.94