Model-Checking Iterated Games

Huang, Chung-Hao, Schewe, Sven ORCID: 0000-0002-9093-9518 and Wang, Farn
(2013) Model-Checking Iterated Games. In: Tools and Algorithms for the Construction and Analysis of Systems, Rome, Italy.

[img] Text
paper_240.pdf - Submitted version

Download (253kB)


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. © 2013 Springer-Verlag.

Item Type: Conference or Workshop Item (Unspecified)
Additional Information: ## TULIP Type: Conference Proceedings (contribution) ##
Depositing User: Symplectic Admin
Date Deposited: 22 Feb 2017 10:38
Last Modified: 19 Jan 2023 07:19
DOI: 10.1007/978-3-642-36742-7_11
Related URLs: