×

Decidable extensions of Church’s problem. (English) Zbl 1257.03034

Grädel, Erich (ed.) et al., Computer science logic. 23rd international workshop, CSL 2009, 18th annual conference of the EACSL, Coimbra, Portugal, September 7–11, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-04026-9/pbk). Lecture Notes in Computer Science 5771, 424-439 (2009).
Summary: For a two-variable formula \(B(X,Y)\) of monadic logic of order (MLO) the Church synthesis problem concerns the existence and construction of a finite-state operator \(Y=F(X)\) such that \(B(X,F(X))\) is universally valid over Nat.
J. R. Büchi and L. H. Landweber [Trans. Am. Math. Soc. 138, 295–311 (1969; Zbl 0182.02302)] proved that the Church synthesis problem is decidable.
We investigate a parameterized version of the Church synthesis problem. In this extended version a formula \(B\) and a finite-state operator \(F\) might contain as a parameter a unary predicate \(P\).
A large class of predicates \(P\) is exhibited such that the Church problem with the parameter \(P\) is decidable.
Our proofs use the composition method and game-theoretical techniques.
For the entire collection see [Zbl 1175.68011].

MSC:

03B25 Decidability of theories and sets of sentences

Citations:

Zbl 0182.02302
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Nagel, E., et al. (eds.) Proc. International Congress on Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford University Press (1960)
[2] Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finitestate strategies. Transactions of the AMS 138(27), 295–311 (1969) · Zbl 0182.02302 · doi:10.1090/S0002-9947-1969-0280205-0
[3] Carton, O., Thomas, W.: The Monadic Theory of Morphic Infinite Words and Generalizations. Inf. Comput. 176(1), 51–65 (2002) · Zbl 1012.03015 · doi:10.1006/inco.2001.3139
[4] Church, A.: Logic, Arithmetic and Automata. In: Proc. Intrnat. Cong. Math. 1963, Almquist and Wilksells, Uppsala (1963) · Zbl 0116.33604
[5] Elgot, C., Rabin, M.O.: Decidability and Undecidability of Extensions of Second (First) Order Theory of (Generalized) Successor. J. Symb. Log. 31(2), 169–181 (1966) · Zbl 0144.24501 · doi:10.2307/2269808
[6] Grädel, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002) · Zbl 1011.00037 · doi:10.1007/3-540-36387-4
[7] Gurevich, Y.: Monadic second-order theories. In: Barwise, J., Feferman, S. (eds.) Model-Theoretic Logics, pp. 479–506. Springer, Heidelberg (1985)
[8] Feferman, S., Vaught, R.L.: The first-order properties of products of algebraic systems. Fundamenta Mathematica 47, 57–103 (1959) · Zbl 0088.24803
[9] McNaughton, R.: Finite-state infinite games. Project MAC Rep. MIT, Cambridge (1965)
[10] Perrin, D., Pin, J.E.: Infinite Words Automata, Semigroups, Logic and Games. In: Pure and Applied Mathematics, vol. 141. Elsevier, Amsterdam (2004) · Zbl 1094.68052
[11] Rabinovich, A.: On decidability of Monadic logic of order over the naturals extended by monadic predicates. Information and Computation 205(6), 870–889 (2007) · Zbl 1115.68100 · doi:10.1016/j.ic.2006.12.004
[12] Rabinovich, A.: Church Synthesis Problem with Parameters. Logical Methods in Computer Science 3(4:9), 1–24 (2007) · Zbl 1131.03016
[13] Rabinovich, A.: Decidable Extensions of Church’s Problem (full version) (2009), http://www.cs.tau.ac.il/ rabinoa/csl09a-full · Zbl 1257.03034
[14] Rabinovich, A., Thomas, W.: Decidable Theories of the Ordering of Natural Numbers with Unary Predicates. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 562–574. Springer, Heidelberg (2006) · Zbl 1225.03013 · doi:10.1007/11874683_37
[15] Robinson, R.M.: Restricted Set-Theoretical Definitions in Arithmetic. Proceedings of the AMS 9(2), 238–242 (1958) · Zbl 0112.00702 · doi:10.1090/S0002-9939-1958-0093479-4
[16] Semenov, A.: Logical theories of one-place functions on the set of natural numbers. Mathematics of the USSR - Izvestia 22, 587–618 (1984) · Zbl 0541.03005 · doi:10.1070/IM1984v022n03ABEH001456
[17] Shelah, S.: The monadic theory of order. Ann. of Math. 102, 379–419 (1975) · Zbl 0345.02034 · doi:10.2307/1971037
[18] Siefkes, D.: The recursive sets in certain monadic second order fragments of arithmetic. Arch. Math. Logik 17, 71–80 (1975) · Zbl 0325.02033 · doi:10.1007/BF02280817
[19] Thomas, W.: Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In: Mycielski, J., Rozenberg, G., Salomaa, A. (eds.) Structures in Logic and Computer Science. LNCS, vol. 1261, pp. 118–143. Springer, Heidelberg (1997) · Zbl 0888.03002 · doi:10.1007/3-540-63246-8_8
[20] Trakhtenbrot, B.A.: Finite automata and the logic of one-place predicates (Russian version 1961). AMS Transl. 59, 23–55 (1966) · Zbl 0192.07801
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.