On the Relationship Between Monadic and Weak Monadic Second Order Logic on Arbitrary Trees, with Applications to the mu-Calculus

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

Abstrakty

EN

In 1970, in Weakly definable relations and special automata, Math. Log. and Found. of Set Theory, pp 1-23, Rabin shows that a language is recognizable by a tree automaton with Büchi like infinitary condition if and only if it is definable as the projection of a weakly definable language. In this paper, we refine this result characterizing such languages as those definable in the monadic Σ₂ level of the quantifier alternation depth hierarchy of monadic second order logic (MSO). This new result also contributes to a better understanding of the relationship between the quantifier alternation depth of hierarchy of MSO and the fixpoint alternation depth hierarchy of the mu-calculus: it shows that the bisimulation invariant fragment of the monadic Σ₂ level equals the νμ-level of the mu-calculus hierarchy.

Słowa kluczowe

EN

infinitesimal geometry; finite state machine; numerical analysis; mathematical analysis; semantics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 61, nr 3,4
• Strony: 247--265
• Opis fizyczny: Bibliogr. 30 poz.

Twórcy

autor

Janin D.

• LaBRI, Universite Bordeaux I, 351 cours de la Liberation, F-33405 Talence cedex, France

autor

Lenzi G.

• Dipartimento di Matematica Università di Pisa via iiuonarroti 2, 1-5612 7 Pisa, Italy

Bibliografia

• [1] Arnold, A.: The mu-calculus alternation-depth hierarchy over the binary tree is strict. Theoretical Informatics and Applications, 33, 1999, 329-339.
• [2] Arnold, A., Niwiński, D.: Rudiments of mu-calculus. Studies in Logic and the Foundations of Mathematics vol. 146, North-Holland, 2001.
• [3] Bradfield, J.: The modal mu-calculus alternation hierarchy is strict. Theoretical Comp. Science, 195, 1998, 133-153.
• [4] Büchi, J. R.: On a decision method in restricted second order arithmetic. Proceedings of the international congress on Logic, Methodology and Philosophy of Science I960, Stanford University Press, 1962,1-11.
• [5] Courcelle, B.: The Monadic Second Order Logic Of Graph I: Recognizable sets of finite graphs. Inf. And Comp.,85, 1990,12-75.
• [6] Ebbinghaus, H., Flum, J., Thomas, W.: Mathematical Logic, Undergraduate Texts in Mathematics, Springer-verlag, 1984.
• [7] Emerson, E.: Temporal and modal logic, in: Handbook of Theor. Comp. Science (vol. B) (J. Van Leeuwen, Ed.), Elsevier, 1990, 995-1072.
• [8] Gaifman, H.: Modeling Concurrency By Partial Orders and Nonlinear Transition Systems, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, 1988.
• [9] Gradel, E., Thomas, W., Wilke, T, Eds.: Automata, Logics and Infinite Games, LNCS Tutorial 2500, Springer, 2002.
• [10] Janin, D.: Automata, tableaus and a reduction theorem for fixpoint calculi in arbitrary complete lattices, IEEE Symp. on Logic in Computer Science (LICS), 1997,172-182.
• [11] Janin, D., Lenzi, G.: Relating Levels of the Mu-calculus Hierarchy and Levels of the Monadic Hierarchy, IEEE Symp. on Logic in Computer Science (LICS), IEEE Computer Society, 2001, 347-356.
• [12] Janin, D., Lenzi, G.: On the logical definability of topologically closed recognizable languages of infinite trees. Computing and Informatics, 2\,2Q01, 185-203.
• [13] Janin, D., Walukiewicz, I.: Automata for the modal mu-calculus and related results. Mathematical Found, of Comp. Science (MFCS), LNCS 969, 1995.
• [14] Janin, D., Walukiewicz, I.: On the expressive completeness of the modal mu-calculus with respect to monadic second order logic, Conf on Concurrency Theory (CONCUR'96), LNCS 1119, 1996,263-277.
• [15] Kozen, D.: Results on The Propositional μ-calculus. Theoretical Comp. Science, 27, 1983, 333-354.
• [16] Kupferman, O., Vardi, M.: II2 n S2 = AFMC, Int. Call, on Aut., Lang, and Programming (ICALP), LNCS 2719,2003,697-713.
• [17] Lenzi, G.: A new logical characterization of Büchi automata, Symp. on Theor. Aspects of Computer Science (STACS), LNCS 2010, 2001.
• [18] Milner, R.: Communication and concurrency, Prentice-Hall, 1989.
• [19] Mostowski, A.: Hierarchies of weak automata on weak monadic formulas. Theoretical Comp. Science, 83, 1991,323-335.
• [20] Muller, D. E., Saoudi, A., Schupp, P. E.: Alternating automata, the weak monadic theory of trees and its complexity. Theoretical Comp. Science, 97, 1992, 233-244.
• [21] Muller, D. E., Schupp, P. E.: Alternating automata on infinite trees. Theoretical Comp. Science, 54, 1987, 267-276.
• [22] Niwiński, D.: Fixed Points vs. Infinite Generation, Proc. 3rd. IEEE LICS, 1988,402-409.
• [23] Park, D.: Concurrency and automata on infinite sequences, 5th GI Conf. on Theoret. Comput. Sci., LNCS 104, Karlsruhe, 1981, 167-183.
• [24] Pnueli, A.: The Temporal Logic of Programs, 18th Symposium on Foundations of Computer Science, 1977, 46-57.
• [25] Rabin, M. O.: Decidability of second order theories and automata on infinite trees, Trans. Amer. Math. Soc, 141, 1969, 1-35.
• [26] Rabin, M. O.: Weakly definable relations and special automata. Mathematical Logic and Foundation of Set Theory, North Holland, 1970, 1-23.
• [27] Shoenfield, J. R.: Mathematical Logic, Addison-Wesley, Reading, Mass., 1967.
• [28] Skurczyński, J.: A characterization of Büchi tree automata. Information Processing Letters, 81,2002,29-33.
• [29] Thomas, W: Automata on Infinite Objects, in: Handbook of Theor. Comp. Science (vol. B) (J. Van Leeuwen, Ed.), Elsevier, 1990,133-191.
• [30] Walukiewicz, I.: Monadic second order logic on tree-like structures, Symp. on Theor Aspects of Computer Science (STACS), 1996, LNCS 1046. Full version in Information and Computation 164 (2001) pp. 234-263.