Refining and Delegating Strategic Ability in ATL

Dimitar P. Guelev
(Institute of Mathematics and Informatics, Bulgarian Academy of Sciences)

We propose extending Alternating-time Temporal Logic (ATL) by an operator <i refines-to G> F to express that agent i can distribute its powers to a set of sub-agents G in a way which satisfies ATL condition f on the strategic ability of the coalitions they may form, possibly together with others agents. We prove the decidability of model-checking of formulas whose subformulas with this operator as the main connective have the form <i_1 refines-to G_1>...<i_m refines-to G_m> f, with no further occurrences of this operator in f.

In Fabio Mogavero, Aniello Murano and Moshe Y. Vardi: Proceedings 2nd International Workshop on Strategic Reasoning (SR 2014), Grenoble, France, April 5-6, 2014, Electronic Proceedings in Theoretical Computer Science 146, pp. 57–63.
Published: 1st April 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: