来源：期刊VIP网 时间：
作者：凌灿红;常亮;周洁;潘海玉;
单位：桂林电子科技大学广西可信软件重点实验室;上海师范大学数理学院;
摘要：为了对包含多值信息的开放系统进行形式化验证，在多值逻辑的基础上提出了多值交互时序逻辑并研究了该逻辑的模型检验问题。首先，引入多值并发博弈结构作为此类开放系统的模型，该模型的最大特点是可以建模带有多值信息的开放系统。其次，给出基于此模型的多值交互时序逻辑的语法和语义，该逻辑可以描述带有多值信息的待验证属性。最后，基于不动点理论给出多值交互时序逻辑的模型检验算法，并对算法的时间复杂度进行了分析，结果表明，可以在多项式时间内完成对多值交互时序逻辑的模型检验。
关键词：模型检验;;多值逻辑;;交互时序逻辑;;并发博弈结构
基金资助：国家自然科学基金项目(61966009,62162014)
