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:
| File | Dimensione | Formato | |
|---|---|---|---|
|
CICLfinal.pdf
non disponibili
Tipologia:
Documento in Pre-print
Licenza:
Non pubblico
Dimensione
287.23 kB
Formato
Adobe PDF
|
287.23 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
