We show that the vectorial mu-calculus model checking prob-
lem over arbitrary graphs reduces to the vectorial, existential -calculus model checking problem over S5 graphs.We also draw some consequencesof this fact. Moreover, we give a proof that satisability of -calculus in S5 is NP-complete, and by using S5 graphs we give a new proof that the
satisability problem of the existential mu-calculus is also NP-complete.
