ATCL:基于承诺的agent组织描述工具  

ATCL:formalization tool for commitment-based agent organization

作　　者：傅朝阳[1,2] 高济[1] 周尤明[1] 

机构地区：[1]浙江大学人工智能研究所,浙江杭州310027 [2]苏州科技学院电子系,江苏苏州215011

出　　处：《浙江大学学报（工学版）》2011年第4期627-636,共10页Journal of Zhejiang University：Engineering Science

基　　金：国家"973"重点基础研究发展规划资助项目(2003CB317005);国家"863"高技术研究发展计划资助项目(2007AA01Z187);国家自然科学基金资助项目(60775029);浙江省自然科学基金资助项目(Y1090734)

摘　　要：针对当前描述agent组织的逻辑无法刻画组织间及组织内部可以判定的并发活动这一问题,提出带有截止期限承诺语义的交互时态承诺逻辑,用于描述基于信任的协作.通过引入承诺,将ATL的合作算子《》扩展为《C:ξ:ω:Θ》,表示:组织C承诺当条件ξ满足时立刻开始按规划ω执行,保证在Θ成立之前实现某商定内容.建立交互时态承诺逻辑(ATCL).给出基于行为的迁移系统,以此建模基于带有截至期限条件承诺的agent组织,分别给出ATCL的语法和语义.给出模型检测算法,证明了ATCL的模型检测复杂度为PTIME-complete.以卫星图像服务领域特定场景为例,展示了ATCL的表达能力,为研究agent组织可信协作提供了较好的形式化工具.Current logics depicting agent organizations can＇t present the decidable concurrent activities between or inside agent organizations. The alternating-time temporal commitment logic was proposed in order to solve the problem, which is based on the semantics of commitment with deadline and can unfold the trust based cooperation. The cooperation modality of ATL was extended into 《C：ξ：ω：Ξ》 by incorporating the commitment semantics to present that the coalition C promises to cooperate to achieve something before ω satisfied by executing according to the plan of Ξ once the condition ξ becomes true. The action-based transition system was conducted and then the agent organization on the conditional commitment with deadline. Furthermore, the lexical rules and semantics of ATCL were introduced. The model checking algorithm of ATCL was provided and the complexity of the algorithm was proved to be PTIME-complete. An example to demonstrate the capability of ATCL was given depicting a satellite imaging domain specific scenario. ATCL is a well-constructed formalization tool for studying the trusted cooperation between agent organizations.

关 键 词：承诺 AGENT组织 交互时态逻辑 交互时态承诺逻辑 

分 类 号：TP302.2[自动化与计算机技术—计算机系统结构]