高级检索
    刘万伟 王 戟 陈火旺. 基于Game理论的μ-演算公理化[J]. 计算机研究与发展, 2007, 44(11): 1896-1902.
    引用本文: 刘万伟 王 戟 陈火旺. 基于Game理论的μ-演算公理化[J]. 计算机研究与发展, 2007, 44(11): 1896-1902.
    Liu Wanwei, Wang Ji, and Chen Huowang. A Game-Based Axiomatization of μ-Calculus[J]. Journal of Computer Research and Development, 2007, 44(11): 1896-1902.
    Citation: Liu Wanwei, Wang Ji, and Chen Huowang. A Game-Based Axiomatization of μ-Calculus[J]. Journal of Computer Research and Development, 2007, 44(11): 1896-1902.

    基于Game理论的μ-演算公理化

    A Game-Based Axiomatization of μ-Calculus

    • 摘要: 随着软硬件系统复杂性的不断提高,各种验证技术被越来越广泛的使用.模型检验技术是一种保证软硬件设计、实现正确性的有效技术.在针对软硬件的模型验证技术中,一般采用时序逻辑作为规约语言.模态μ-演算是模态和时序逻辑中应用较为广泛的一种,它具有语法成分简洁、表达能力强等特点.扩展了Lange和Stirling基于Focus Game的LTL和CTL的公理化方法.提出了一种基于Game理论的μ-演算公式的可满足性的测试方法,该种方法能够将模态μ-演算公式的可满足性问题转化为Focus Game的求解问题.进一步,基于这套Game规则,给出了一个新的关于μ-演算可靠完备的推理系统.同已有的μ-演算公理系统相比,该推理系统相对直观、简洁.

       

      Abstract: With the never-ending growth of the complexity of modern hardware and software systems, more and more sophisticated methods of verification are required. Model checking has been proved to be an effective approach to guaranteeing the correctness of design and implementation of software and hardware system. Model and temporal logics are used as specification languages in software and hardware verification. Modal μ-calculus is an extremely popular and important one among these logics. It is succinct in syntax and powerful in expressiveness. Since Kozen's paper on modal μ-calculus, it has received ever growing interest in both theoretical and application aspects. Based on the focus game theory, Lange and Stirling proposed the axiom systems for LTL and CTL. This paper extends that idea to that for modal μ-calculus. A game-theoretic approach is presented to test the satisfiability of modal μ-calculus formulas. In addition, this approach converts the satisfiability problem for μ-calculus into a solving problem for focus games. Consequently, based on these game rules, an axiom system for μ-calculus is developed, and the completeness of this deductive system can be proved via the game based satisfiability testing procedure. By comparison, this axiom system is much more intuitive and succinct than the existing μ-calculus axiom systems.

       

    /

    返回文章
    返回