On modal mu-calculus in S5 and application

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