中文摘要：

针对当前描述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.