论文部分内容阅读
随着软硬件系统复杂性的不断提高，各种验证技术被越来越广泛的使用．模型检验技术是一种保证软硬件设计、实现正确性的有效技术．在针对软硬件的模型验证技术中，一般采用时序逻辑作为规约语言．模态口一演算是模态和时序逻辑中应用较为广泛的一种，它具有语法成分简洁、表达能力强等特点．扩展了Lange和Stirling基于FocusGame的LTL和CTL的公理化方法．提出了一种基于Game理论的肛一演算公式的可满足性的测试方法，该种方法能够将模态μ-演算公式的可满足性问题转化为FocusGame的求解问题．进一步，基于这