On Modal μ-Calculus in S5 and Applications

We consider the mu-calculus over graphs where the accessibility relation is an equivalence (S5-graphs). We show that the vectorial mu-calculus model checking problem over arbitrary graphs reduces to the vectorial, existential mu-calculus model checking problem over S5 graphs. Moreover, we give a proof that satisfiability of mu-calculus in S5 is NP-complete, and by using S5 graphs we give a new proof that the satisfiability problem of the existential mu-calculus is also NP-complete. Finally we prove that on multimodal S5, in contrast with the monomodal case, the fixpoint hierarchy of the mu-calculus is infinite and the finite model property fails.