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