Shelah-Stupp’s Iteration and Muchnik’s Iteration

• Autorzy: Caucal D. , Knapik T.

Identyfikatory

DOI

10.3233/FI-2018-1667

• Języki publikacji: EN

Abstrakty

EN

In the early seventies, Shelah proposed a model-theoretic construction, nowadays called “iteration”. This construction is an infinite replication in a tree-like manner where every vertex possesses its own copy of the original structure. Stupp proved that the decidability of the monadic second-order (MSO) theory is transferred from the original structure onto the iterated one. In its extended version discovered by Muchnik and introduced by Semenov, the iteration became popular in computer science logic thanks to a paper by Walukiewicz. Compared to the basic iteration, Muchnik’s iteration has an additional unary predicate which, in every copy, marks the vertex that is the clone of the possessor of the copy. A widely spread belief that this extension is crucial is formally confirmed in the paper. Two hierarchies of relational structures generated from finite structures by MSO interpretations and either Shelah-Stupp’s iteration or Muchnik’s iteration are compared. It turns out that the two hierarchies coincide at level 1. Every level of the latter hierarchy is closed under Shelah-Stupp’s interation. In particular, the former hierarchy collapses at level 1.

Słowa kluczowe

EN

infinite-state systems; structure-building operations; Shelah-Stupp’s iteration; Muchnik’s iteration

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 159, nr 4
• Strony: 327--359
• Opis fizyczny: Bibliogr. 36 poz., rys.

Twórcy

autor

Caucal D.

• LIGM–CNRS, Université Paris-Est, 77454 Marne-la-Vallée Cedex 2, France

autor

Knapik T.

• ISEA, Université de la Nouvelle Calédonie, 98851 Nouméa Cedex, France

Bibliografia

• [1] Courcelle B. The Expression of Graph Properties and Graph Transformations in Monadic Second-Order Logic. In: Rozenberg G (ed.), Handbook of Graph Grammars and Computing by Graph Transformation, volume 1, pp. 313-400. World Scientific, 1997. ISBN: 98-102288-48.
• [2] Büchi JR. On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Congr). Stanford University Press, 1962 pp. 1-11.
• [3] Trakhtenbrot B. Finite automata and the logic of monadic predicates. Doklady Akademii Nauk SSSR, 1961. 140:326-329.
• [4] Elgot CC. Decision Problems for Finite Automata Design and Related Arithmetics. Transactions of the American Mathematical Society, 1961. 98:21-52. doi:10.2307/1993511.
• [5] Rabin MO. Decidability of Second-order Theories and Automata on Infinite Trees. Transactions of the American Mathematical Society, 1969. 141:1-35. URL http://www.jstor.org/stable/1995086.
• [6] Shelah S. The Monadic Theory of Order. Annals of Mathematics, 1975. 102:379-419. doi:10.2307/1971037.
• [7] Stupp J. The Lattice Model is Recursive in the Original Model. The Hebrew University, 1975.
• [8] Courcelle B, Engelfriet J. Graph structure and Monadic Second-Order Logic, a Language Theoretic Approach. Cambridge University Press, 2012. ISBN:0521898331, 9780521898331.
• [9] Semenov AL. Decidability of Monadic Theories. In: Chytil M, Koubek V (eds.), Mathematical Foundations of Computer Science, LNCS 176. Springer, Praha, 1984 pp. 162-175.
• [10] Walukiewicz I. Monadic second-order logic on tree-like structures. Theoretical Computer Science, 2002. 275(1-2):311-346. doi:10.1016/S0304-3975(01)00185-2.
• [11] Muller DE, Schupp PE. The Theory of Ends, Pushdown Automata and Second-order Logic. Theoretical Computer Science, 1985. 37:51-75. URL https://doi.org/10.1016/0304-3975(85)90087-8.
• [12] Caucal D. On the Regular Structure of Prefix Rewriting. Theoretical Computer Science, 1992. 106:61-86. doi:10.1016/0304-3975(92)90278-N.
• [13] Courcelle B. The Monadic Second-order Logic of Graphs, II: Infinite Graphs of Bounded Width. Mathematical System Theory, 1989. 21:187-221. doi:https://doi.org/10.1007/BF02088013.
• [14] Courcelle B. The Monadic Second-order Logic of Graphs, VII: Graphs as Relational Structures. Theoretical Computer Science, 1992. 101:3-33. URL https://doi.org/10.1016/0304-3975(92)90148-9.
• [15] Barthelmann K. On Equational Simple Graphs. Technical Report 9/97, Johannes Gutenberg Universität, Mainz, 1998.
• [16] Caucal D. On Infinite Transition Graphs Having a Decidable Monadic Second-order Theory. Theoretical Computer Science, 2003. 290(1):79-115. doi:10.1016/S0304-3975(01)00089-5.
• [17] Siefkes D. Decidable Extensions of Monadic Second-order Successor Arithmetics. Mannheim: Bibilogr. Inst., 1969 pp. 341-472.
• [18] Elgot CC, Rabin MO. Decidability and Undecidability of Extensions of the Second-order Theory of Successor. Journal of Symbolic Logic, 1966. 31:169-181. doi:10.2307/2269808.
• [19] Thomas W. The Theory of Successor with an Extra Predicate. Mathematische Annalen, 1978. 237:121-132. URL https://doi.org/10.1007/BF01351676.
• [20] Caucal D. Sur des graphes infinis réguliers. Habilitation, Université de Rennes I, 1998.
• [21] Courcelle B, Walukiewicz I. Monadic Second-Order Logic, Graph Coverings and Unfoldings of Transition Systems. Annals of Pure and Applied Logic, 1998. 92:35-62. URL https://doi.org/10.1016/S0168-0072(97)00048-1.
• [22] Knapik T, Niwiński D, Urzyczyn P. Deciding Monadic Theories of Hyperalgebraic Trees. In: Abramsky S (ed.), 5th International Conference on Typed Lambda Calculi and Applications, LNCS 2044. Kraków, 2001 pp. 253-267. doi:10.1007/3-540-45413-6_21.
• [23] Knapik T, Niwiński D, Urzyczyn P. Higher-Order Pushdown Trees are Easy. In: Nielsen M, Engberg U (eds.), FoSSaCS, LNCS 2303. Grenoble, 2002 pp. 205-222. doi:10.1007/3-540-45931-6_15.
• [24] Engelfriet J, Schmidt EM. IO and OI. I. Journal of Computer and System Sciences, 1977. 15:328-353. URL https://doi.org/10.1016/S0022-0000(77)80034-2.
• [25] Damm W. The IO- and OI-hierarchies. Theoretical Computer Science, 1982. 20(2):95-208. URL https://doi.org/10.1016/0304-3975(82)90009-3.
• [26] Caucal D. On Infinite Terms Having a Decidable Monadic Theory. In: Diks K, Rytter W (eds.), MFCS ’2002, LNCS 2420. Springer, Warsaw, 2002 pp. 165-176. doi:10.1007/3-540-45687-2_13.
• [27] Knapik T, Niwiński D, Urzyczyn P, Walukiewicz I. Unsafe Grammars and Panic Automata. In: Caires L, Italiano GF, Monteiro L, Palamidessi C, Yung M (eds.), ICALP, LNCS 3580. Lisbon, 2005 pp. 1450-1461.
• [28] Ong CL. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In: LICS. 2006 pp. 81-90. doi:10.1109/LICS.2006.38.
• [29] Carayol A, Wöhrle S. The Caucal Hierarchy of Infinite Graphs in Terms of Logic and Higher-Order Pushdown Automata. In: FSTTCS, volume 2914 of Lecture Notes in Computer Science. 2003 pp. 112-123. doi:10.1007/978-3-540-24597-1_10.
• [30] Blumensath A. Axiomatising Tree-Interpretable Structures. Theory of Computing Systems, 2004. 37(1):3-27. doi:10.1007/s00224-003-1104-8.
• [31] Karhumäki J, Kunc M, Okhotin A. Computing by commuting. Theor. Comput. Sci., 2006. 356(1-2):200-211. doi:10.1016/j.tcs.2006.01.051.
• [32] Altenbernd J. Reachability over word rewriting systems. Ph.D. thesis, RWTH Aachen University, 2009.
• [33] Angluin D, and Hoover DN. Regular prefix relations. Mathematical systems theory, 1984. 17(3):167-191. doi:10.1007/BF01744439.
• [34] Läuchli H, and Savioz C. Monadic Second Order Definable Relations on the Binary Tree J. Symbolic Logic, 1987. 52(1):219-226. doi:10.2307/2273878.
• [35] Carayol A, and Colcombet T. On Equivalent Representations of Infinite Structures. In: ICALP, volume 2719 of Lecture Notes in Computer Science. 2003 pp. 599-610. doi:10.1007/3-540-45061-0_48.
• [36] Weyer M. Decidability of S1S and S2S. In: Grädel E, Thomas W, Wilke T (eds.), Automata, Logics, and Infinite Games: A Guide to Current Research, volume LNCS 2500. 2001 pp. 207-230. doi:10.1007/3-540-36387-4_12.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).