时序协作逻辑(Temporal Cooperation Logic)是软件模型检测领域的博弈逻辑分支上的重要成果。它扩展了交互时间逻辑(Alternating-time Temporal Logic)[1]，完善了基本策略交互逻辑[12]，允许博弈策略的连续定义，可以比前两者更完美地描述博弈参与者为达到时序目标所需要的协作行为[2]。与其他有相似能力的博弈逻辑相比，时序协作逻辑在表达能力和验证效率之间找到了很好的平衡，因此更加贴近工业化应用。　　本文对时序协作逻辑做出扩展，希望进一步增加其逻辑表达能力，同时合理控制扩展后的逻辑的验证效率，从而继续推进其工业化应用进程。时序协作逻辑要求所有参与协作的博弈者必须是已知的，而本文扩展后的逻辑，可以描述在参与者全集确定的情况下，存在未知的博弈者参与的协作行为。本文又对扩展后的逻辑设计并实现了语法解析器和模型检测方法，并利用现实场景案例获得了详尽的实验数据。实验证明，扩展后的逻辑提高了时序协作逻辑的表达能力，同时拥有良好的时间效率。　　具体而言，本文主要研究工作与成果如下:　　(1)扩展了时序协作逻辑，允许在参与者全集确定的情况下，在为达到时序目标所需要的协作行为中，出现未知的博弈者，并允许通过一系列运算符来限制未知博弈者的候选范围。　　(2)为扩展后的逻辑设计并实现了语法解析器，可以解析以DOT绘图语言所描述的模型和需要验证的扩展时序博弈逻辑性质。用户可以通过DOT绘图工具将模型和需要验证的性质绘制成图，从而获得更加直观的了解。　　(3)为扩展后的逻辑设计并实现了模型检测方法，可以验证性质的可满足性，并找出所需条件。　　(4)利用现实场景案例获得了详尽的实验数据，证明扩展时序协作逻辑拥有更强的逻辑表达能力和良好的时间效率。