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.
On modal mu-calculus in S5 and application
D'AGOSTINO, Giovanna;
2011-01-01
Abstract
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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
