Refining strategic ability in alternating-time temporal logic

We propose extending Alternating-time Temporal Logic (ATL) by a unary operator 〈i⊑Γ〉 about distributing the powers of some given agent i to a given set of sub-agents Γ. 〈i⊑Γ〉φ means that i's powers can be distributed in a way which satisfies the ATL condition φ on the strategic ability of the coalitions the members of Γ may form, possibly together with others agents. We prove the decidability of model checking of formulas whose 〈.⊑.〉-subformulas have the form 〈i1⊑Γ1〉…〈im⊑Γm〉φ, with no further occurrences of 〈.⊑.〉 in φ. We also give some axioms and proof rules about the new operator.