Huang, Chung-Hao, Schewe, Sven 
ORCID: 0000-0002-9093-9518 and Wang, Farn
(2017)
Model-checking iterated games.
ACTA INFORMATICA, 54 (7).
pp. 625-654.
![[img]](https://livrepository.liverpool.ac.uk/style/images/fileicons/text.png) |
Text
ppAI2016.pdf - Author Accepted Manuscript Download (468kB) |
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 NL complete in the model. This advancement over nonelementary logics is bought by disallowing a too close entanglement between the cooperation and competition. We show how allowing such an entanglement immediately leads to a nonelementary complexity. We have implemented a model checker for the logic and shown the feasibility of model checking on a few benchmarks.
| Item Type: | Article |
|---|---|
| Depositing User: | Symplectic Admin |
| Date Deposited: | 23 Sep 2016 11:19 |
| Last Modified: | 19 Jan 2023 07:30 |
| DOI: | 10.1007/s00236-016-0277-y |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3003307 |
Dimensions
Dimensions
