On Modal μ-Calculus in S5 and Applications

• Autorzy: D'Agostino G. , Lenzi G.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

my-calculus; equivalence relation; model checking; parity games; S5

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 124, nr 4
• Strony: 465--482
• Opis fizyczny: Bibliogr. 16 poz.

Twórcy

autor

D'Agostino G.

• Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100 Udine, Italy

autor

Lenzi G.

• Dipartimento di Matematica e Informatica, Università di Salerno, Via Ponte Don Melillo 1, 84084 Fisciano (SA), Italy

Bibliografia

• [1] Alberucci, L.: Sequent Calculi for the Modal μ-Calculus over S5, J. Log. Comput., 19(6), 2009, 971-985.
• [2] Alberucci, L., Facchini, A. : The modal mu-calculus hierarchy over restricted classes of transition systems, Journal of Symbolic Logic, 74, 2009, 1367-1400.
• [3] Arnold, A.: The μ-Calculus alternation-depth hierarchy is strict on binary trees, Theoretical Informatics and Applications, 33, 1999, 329-339.
• [4] Arnold, A., Niwinski, D.: Rudiments of μ-calculus, North-Holland, 2001.
• [5] Clarke, E. M. Jr., Grumberg, O., Peled, D. A.: Model Checking, MIT Press, 1999.
• [6] D’Agostino, G., Lenzi, G. : On the i-calculus over Transitive and Finite Transitive Frames, Theoretical Computer Science, 441, 2010, 4273-4290.
• [7] Dawar, A., Otto, M.: Modal Characterisation Theorems over Special Classes of Frames, Annals of Pure and Applied Logic, 161, 2009, 1-42.
• [8] Emerson, E. A. : Model Checking and the Mu-calculus. Descriptive Complexity and Finite Models, 1996, 185-214.
• [9] Emerson, E. A., Jutla, C. S.: Tree Automata, Mu-Calculus and Determinacy (Extended Abstract). FOCS , 1991, 368-377.
• [10] Fagin, R.: Reasoning about knowledge, MIT Press, 2003.
• [11] Henzinger, T. A., Kupferman, O., Majumdar, R. : On the Universal and Existential Fragments of the Mu- Calculus, Theoretical Computer Science 354 , 2006, 173-186.
• [12] Jurdzinski, M. : Deciding the winner in parity games is in UP n co — UP, Inform. Proc. Letters 68, 1998, 119-124.
• [13] Kozen, D.: Results on the propositional i-calculus, Theoretical Computer Science, 27, 1983, 333-354.
• [14] Mader, A.: Verification of Modal Properties using Boolean Equation Systems, Ph. D. Thesis, 1997.
• [15] Martin, D. A.: Borel determinacy, Ann. Math., 102, 1975, 363-371.
• [16] Obdrzalek, J.: Fast Mu-calculus model checking when tree width is bounded, Proceedings of CAV 2003, Springer LNCS 2725, 80-92.