Abstract
Church’s Problem (1962) asks for the construction of a procedure which, given a logical specification ϕ on sequence pairs, realizes for any input sequence X an output sequence Y such that (X,Y) satisfies ϕ. Büchi and Landweber (1969) gave a solution for MSO specifications in terms of finite-state automata. We address the problem in a more general logical setting where not only the specification but also the solution is presented in a logical system. Extending the result of Büchi and Landweber, we present several logics \({\cal L}\) such that Church’s Problem with respect to \({\cal L}\) has also a solution in \({\cal L}\), and we discuss some perspectives of this approach.
This paper was written during a visit of the first author in Aachen in February 2007, funded by the European Science Foundation ESF in the Research Networking Programme AutoMathA (Automata: From Mathematics to Applications).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, 367–378 (1969)
Büchi, J.R., Elgot, C.C., Wright, J.B.: The nonexistence of certain algorithms of finite automata theory. Notices of the AMS 5, 98 (1958)
Church, A.: Logic, arithmetic, and automata. In: Proc. Int. Congr. Math. 1962, Inst. Mittag-Lefler, Djursholm, Sweden, pp. 23–35 (1963)
Dziembowski, S., Jurdziński, M., Walukiewicz, I.: How much memory is needed to win infinite games? In: Proc. 12th LICS, pp. 99–110 (1997)
Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Springer, Heidelberg (1995)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Gurevich, Y., Harrington, L.: Trees, automata, and games. In: Proc. 14th STOC, pp. 60–65. ACM Press, New York (1982)
Gurevich, Y.: Monadic second order theories. In: Barwise, J., Feferman, S. (eds.) Model Theoretic Logics, pp. 479–506. Springer, Heidelberg (1986)
Kupferman, O., Vardi, M.Y.: On Bounded Specifications. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 24–38. Springer, Heidelberg (2001)
Moschovakis, Y.: Descriptive Set Theory. North-Holland, Amsterdam (1980)
Perrin, D., Pin, J.E.: Infinite Words. Elsevier, Amsterdam (2004)
Pin, J.E.: Varieties of Formal Languages. North Oxford and Pergamon, Oxford (1986)
Putnam, H.: Decidability and essential undecidability. JSL 22, 39–54 (1957)
Rabinovich, A.: Church Synthesis Problem with Parameters. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 546–561. Springer, Heidelberg (2006)
Selivanov, V.: Fine hierarchy of regular aperiodic ú- languages. In: Harju, T., et al. (eds.) DLT 2007. LNCS, vol. 4588, Springer, Heidelberg (2007)
Shelah, S.: The monadic theory of order. Ann. of Math. 102, 349–419 (1975)
Straubing, H.: Finite Automata, Formal Logic, and Circuit Complexity, Birkhäuser, Boston (1994)
Thomas, W.: A combinatorial approach to the theory of ω-automata. Inf. Contr. 48, 261–283 (1981)
Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)
Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. 3, pp. 389–455. Springer, Heidelberg (1997)
Thomas, W.: Complementation of Büchi automata revisited. In: Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pp. 109–120. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rabinovich, A., Thomas, W. (2007). Logical Refinements of Church’s Problem. In: Duparc, J., Henzinger, T.A. (eds) Computer Science Logic. CSL 2007. Lecture Notes in Computer Science, vol 4646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74915-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-74915-8_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74914-1
Online ISBN: 978-3-540-74915-8
eBook Packages: Computer ScienceComputer Science (R0)