ATL中战略能力的提炼与委派
Refining and Delegating Strategic Ability in ATL
摘要：
我们建议扩展交替时间时序逻辑（ATL）的运营商<i refines-to G>F表示，代理i可以分配其权力的一组子代理G的方式，满足ATL条件f的战略能力，他们可能形成的联盟，可能与其他代理。证明了以该算子为主要连接符的子公式具有如下形式的公式的模型检验的可判定性<i_1 refines-to G_1>。<i_m refines-to G_m>f，在f中不再出现该运算符。
英文摘要：
We propose extending Alternating-time Temporal Logic (ATL) by an operator <i refines-to G> 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 <i_1 refines-to G_1>...<i_m refines-to G_m> f, with no further occurrences of this operator in f.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
