Article ID Journal Published Year Pages File Type
4950714 Information and Computation 2017 13 Pages PDF
Abstract
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.
Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
,