Abstract:

Fuzzy concurrent game structures are a tool to model and analyze open systems with fuzzy uncertain information, and the model checking problem for fuzzy alternating-time temporal logic over these models has been explored yet. This paper first transforms model checking problem for fuzzy alternating-time temporal logic into several classical alternating-time temporal logic model checking problems, and then uses the algorithms for alternating-time temporal logic model checking problem to solve the problem. This paper also discusses the continuity property of semantics of fuzzy alternating-time temporal logic. In other words, when arbitrarily small changes happen over fuzzy concurrent game structures, small changes happen or not in truth values of fuzzy alternating-time temporal logic formulas.

Key words: alternating-time temporal logic, computation tree logic, concurrent game structure, model checking, fuzzy logic

摘要：

模糊并发博弈结构是一种可以对具有模糊不确定信息的开放系统进行建模和分析的工具，基于该模型的模糊交互时态逻辑的模型检测问题初步得到解决。首先通过将模糊交互时态逻辑的模型检测问题转化为有限个经典的交互时态逻辑的模型检测问题，从而可以利用经典的交互时态逻辑的模型检测算法来解决模糊交互时态逻辑的模型检测；研究了模糊交互时态逻辑语义的连续性问题，即模糊并发博弈结构发生微小变化时，模糊交互时态逻辑的语义是否也相应地发生微小的变化。

关键词: 交互时态逻辑, 计算树逻辑, 并发博弈结构, 模型检测, 模糊逻辑