论文部分内容阅读
针对当前描述agent组织的逻辑无法刻画组织间及组织内部可以判定的并发活动这一问题，提出带有截止期限承诺语义的交互时态承诺逻辑，用于描述基于信任的协作．通过引入承诺，将ATL的合作算子《》扩展为《C：ξ：ω：Ξ》，表示：组织C承诺当条件ξ满足时立刻开始按规划ω执行，保证在Ξ成立之前实现某商定内容．建立交互时态承诺逻辑（ATCL）．给出基于行为的迁移系统，以此建模基于带有截至期限条件承诺的agent组织，分别给出ATCL的语法和语义．给出模型检测算法，证明了ATCL的模型检测复杂度为PTIME—comple