Affiliations: Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100 Udine, Italy. [email protected] | Dipartimento di Matematica e Informatica, Università di Salerno, Via Ponte Don Melillo 1, 84084 Fisciano (SA), Italy. [email protected]
Note: [] Address for correspondence: Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100 Udine, Italy
Abstract: We consider the μ-calculus over graphs where the accessibility relation is an equivalence (S5-graphs). We show that the vectorial μ-calculus model checking problem over arbitrary graphs reduces to the vectorial, existential μ-calculus model checking problem over S5 graphs. Moreover, we give a proof that satisfiability of μ-calculus in S5 is NP-complete, and by using S5 graphs we give a new proof that the satisfiability problem of the existential μ-calculus is also NP-complete. Finally we prove that on multimodal S5, in contrast with the monomodal case, the fixpoint hierarchy of the μ-calculus is infinite and the finite model property fails.
Keywords: μ-Calculus, Parity Games, Equivalence Relations, S5, Model Checking
