Electronic Proceedings in Theoretical Computer Science (Apr 2014)

Refining and Delegating Strategic Ability in ATL

  • Dimitar P. Guelev

Journal volume & issue
Vol. 146, no. Proc. SR 2014
pp. 57 – 63


Read online

We propose extending Alternating-time Temporal Logic (ATL) by an operator 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 ... f, with no further occurrences of this operator in f.