Alternating-time temporal logic has been widely used as the specification language of open systems,and its model checking is one of the most important verification methods for open systems.To describe and check the properties of the open systems with fuzzy uncertainty information,we propose fuzzy alternating-time temporal logic and discuss its model-checking problem.Firstly,we present two semantics,the path semantics and the fixed point semantics,which are equal in value.Based on the result,the model-checking algorithm is given and its time complexity is discussed.%交互时态逻辑已被广泛应用于开放系统的规范描述,交互时态逻辑的模型检测技术是一个比较重要的验证方法.为了形式化描述和验证具有模糊不确定性信息的开放系统的性质,提出了一种模糊交互时态逻辑,并讨论了它的模型检测问题.首先,引入了模糊交互时态逻辑的基于路径和基于不动点的两种语义,证明了其等价性.然后,基于其等价性,给出了模糊交互时态逻辑的模型检测算法和复杂性分析.
展开▼
