Fixpoints and program looping: Reductions from the Propositional mu-calculus into Propositional Dynamic Logics of Looping

Abstract

The propositional mu-calculus is a propositional logic of programs which incorporates a least fixpoint operator and subsumes the Propositional Dynamic Logic of Fischer and Ladner, the infinite looping constructs of Streett and Sherman, and the Game Logic of Parikh. The propositional mu-calculus is strictly stronger in expressive power than any of these other logics. However, the mu-calculus satisfiability problem is polynomially reducible to the satisfiability problem for Propositional Dynamic Logic with Streett's looping construct. This result shows the connection between fixpoints and program looping, provides an alternative decision procedure for the mu-calculus, and rules out the possibility that the complexities of the two logics could be separated by new upper and lower bound results. We also give reductions from several weaker mu-calculi (including those investigated by Kozen, Vardi and Wolper) into variants of Propositional Dynamic Logic with weaker looping constructs (including Sherman's looping construct). The deterministic exponential time upper bounds obtained for these mu-calculi may also be obtained via these reductions.