×

zbMATH — the first resource for mathematics

On the \(\mu \)-calculus over transitive and finite transitive frames. (English) Zbl 1208.68145
Summary: We prove that the modal \(\mu \)-calculus collapses to first order logic over the class of finite transitive frames. The proof is obtained by using some byproducts of a new proof of the collapse of the \(\mu \)-calculus to the alternation free fragment over the class of transitive frames.
Moreover, we prove that the modal \(\mu \)-calculus is Büchi and co-Büchi definable over the class of all models where, in a strongly connected component, vertexes are distinguishable by means of the propositions they satisfy.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B45 Modal logic (including the logic of norms)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Arnold, A.; Niwinski, D., Rudiments of \(\mu\)-calculus, (2001), North-Holland · Zbl 0968.03002
[2] Alberucci, L.; Facchini, A., The modal \(\mu\)-calculus hierarchy over restricted classes of transition systems, J. symbolic logic, 74, 4, 1367-1400, (2009) · Zbl 1191.03012
[3] Arnold, A., The \(\mu\)-calculus alternation-depth hierarchy is strict on binary trees, Ita, 33, 4/5, 329-340, (1999) · Zbl 0945.68118
[4] Bradfield, J., The modal \(\mu\)-calculus alternation hierarchy is strict, Theoret. comput. sci., 195, 133-153, (1998) · Zbl 0915.03017
[5] Clarke, E.; Grumberg, O.; Peled, D., Model checking, (2000), MIT Press
[6] D’Agostino, G.; Lenzi, G., A note on bisimulation quantifiers and fixed points over transitive frames, J. logic comput., 18, 601-614, (2008) · Zbl 1173.03018
[7] D’Agostino, G.; Lenzi, G., On modal \(\mu\)-calculus over finite graphs with bounded strongly connected components, Eptcs, 25, 55-71, (2010)
[8] Janin, D.; Walukiewicz, I., Automata for the modal \(\mu\)-calculus and related results, (), 552-562 · Zbl 1193.68163
[9] Kozen, D., Results on the propositional \(\mu\)-calculus, Theoret. comput. sci., 27, 333-354, (1983) · Zbl 0553.03007
[10] G. Lenzi, The \(\mu\)-calculus and the hierarchy problem, Ph.D. Thesis, Scuola Normale Superiore, Pisa, 1997.
[11] Lenzi, G., The transitive \(\mu\)-calculus is Büchi definable, WSEAS trans. math., 5, 9, 1021-1026, (2006)
[12] Otto, M.; Dawar, A., Modal characterization theorems over special classes of frames, Ann. pure appl. logic, 161, 1-42, (2009) · Zbl 1185.03027
[13] Sambin, G., An effective fixed-point theorem in intuitionistic diagonalizable algebras, Studia logica, 35, 4, 345-361, (1976) · Zbl 0357.02028
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.