Refining and Delegating Strategic Ability in ATL

Dimitar P. Guelev

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.

Knowledge Graph



Sign up or login to leave a comment