Efficient Global Model-Checking for Propositional μ-Calculus

Model-checking algorithms of the propositional μ-calculus fall into two categories: global and local. The state space explosion is the main problem that model-checking algorithms face. How to efficiently lower the time and space complexity of the algorithms is the research focus. Built upon the earlier work by Long, Browne, Jha and Marrero, and according to Tarskis fixpoint theorem, the process of calculating the alternating fixpoint expressions in the propositional μ-calculus, whose alternating nesting depth of fixpoint is 4, is studied carefully. Two groups of partial ordering relation between intermediate results have been found, and a global model-checking algorithm is designed for efficiently evaluating alternating fixpoint expressions in the propositional μ-calculus. This algorithm has a similar time complexity to the earlier work by Long, Browne, Jha and Marrero, i.e., O((2n+1)\+{[d/2]+1}) as opposed to O(n\+{[d/2]+1}), but it has much better space complexity, i.e., polynomial O(dn) as opposed to exponential O(n\+{[d/2]+1}), where n is the number of states in the transition system and d is the alternation depth in the formulas. The contribution is finding out the best global model-checking algorithm whose time complexity is O((2n+1)\+{d/2]+1}) and the space complexity is O(dn).