论文部分内容阅读
交互时态逻辑已被广泛应用于开放系统的规范描述，交互时态逻辑的模型检测技术是一个比较重要的验证方法。为了形式化描述和验证具有模糊不确定性信息的开放系统的性质，提出了一种模糊交互时态逻辑，并讨论了它的模型检测问题。首先，引入了模糊交互时态逻辑的基于路径和基于不动点的两种语义，证明了其等价性。然后，基于其等价性，给出了模糊交互时态逻辑的模型检测算法和复杂性分析。