A Game-Based Axiomatization of μ-Calculus

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.