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.
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) |
Keywords:
fixed points; modal \(\mu \)-calculus; alternation hierarchy; collapse; finite transitive frames; Büchi and co-Büchi definableReferences:
| [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) · Zbl 1456.03035 |
| [8] | Janin, D.; Walukiewicz, I., Automata for the modal \(\mu \)-calculus and related results, (Proceedings of the Conference MFCS’95. Proceedings of the Conference MFCS’95, Lecture Notes in Computer Science, vol. 969 (1995), Springer), 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 \); G. Lenzi, The \(\mu \) |
| [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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
