nach oben

Theory of Computing Systems

Erschienen in:

01.11.2014

On First-Order Logic and CPDA Graphs

verfasst von: Christopher H. Broadbent

Erschienen in: Theory of Computing Systems | Ausgabe 4/2014

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Higher-order pushdown automata (n-PDA) are abstract machines equipped with a nested ‘stack of stacks of stacks’. Collapsible pushdown automata (n-CPDA) extend these devices by adding ‘links’ to the stack and are equi-expressive for tree generation with simply typed λY terms. Whilst the configuration graphs of HOPDA are well understood, relatively little is known about the CPDA graphs. The order-2 CPDA graphs already have undecidable MSO theories but it was only recently shown by Kartzow (Log. Methods Comput. Sci. 9(1), 2013) that first-order logic is decidable at the second level. In this paper we show the surprising result that first-order logic ceases to be decidable at order-3 and above. We delimit the fragments of the decision problem to which our undecidability result applies in terms of quantifer alternation and the orders of CPDA links used. Additionally we exhibit a natural sub-hierarchy enjoying limited decidability.

Vorheriger Artikel Efficient Algorithms for Highly Compressed Data: The Word Problem in Generalized Higman Groups Is in P

Nächster Artikel On the Separation Question for Tree Languages

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

We are very grateful to Arnaud Carayol for suggesting this reduction.

We will only use reachability properties rather than the full μ-calculus. However, the reader unfamiliar with this logic might wish to consult a survey such as [2].

Aehlig, K., de Miranda, J.G., Ong, C.H.L.: Safety is not a restriction at level 2 for string languages. In: Sassone, V. (ed.) Foundations of Software Science and Computational Structures, Proceedings of the 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, 4–8 April 2005. Lecture Notes in Computer Science, vol. 3441, pp. 490–504. Springer, Berlin (2005)

Bradfield, J.C., Stirling, C.P.: Modal logics and mu-calculi: an introduction. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 293–330. Elsevier, Amsterdam (2001) CrossRef

Broadbent, C.H.: On collapsible pushdown automata, their graphs and the power of links. Ph.D. thesis, The University of Oxford, Department of Computer Science (2011)

Broadbent, C.H.: The limits of decidability for first order logic on cpda graphs. In: Dürr, C., Wilke, T. (eds.) 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th, Paris, France, 29 February–3 March 2012. LIPIcs, vol. 14, pp. 589–600. Schloss Dagstuhl/Leibniz-Zentrum fuer Informatik, Berlin (2012)

Broadbent, C.H.: Prefix rewriting for nested-words and collapsible pushdown automata. In: Czumaj, A., Mehlhorn, K., Pitts, A.M., Wattenhofer, R. (eds.) Automata, Languages, and Programming. Proceedings of the 39th International Colloquium, ICALP 2012, Part II, Warwick, UK, 9–13 July 2012. Lecture Notes in Computer Science, vol. 7392, pp. 153–164. Springer, Berlin (2012)

Broadbent, C.H., Carayol, A., Hague, M., Serre, O.: A saturation method for collapsible pushdown systems. In: Czumaj, A., Mehlhorn, K., Pitts, A.M., Wattenhofer, R. (eds.) Automata, Languages, and Programming. Proceedings of the 39th International Colloquium, ICALP 2012, Part II, Warwick, UK, 9–13 July 2012. Lecture Notes in Computer Science, vol. 7392, pp. 165–176. Springer, Berlin (2012)

Broadbent, C.H., Carayol, A., Ong, C.H.L., Serre, O.: Recursion schemes and logical reflection. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, Edinburgh, UK 11–14 July 2010, pp. 120–129. IEEE Computer Society, Los Alamitos (2010) CrossRef

Cachat, T.: Higher order pushdown automata, the Caucal hierarchy of graphs and parity games. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) Automata, Languages and Programming, Proceedings of the 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands 30 June–4 July 2003. Lecture Notes in Computer Science, vol. 2719, pp. 556–569. Springer, Berlin (2003)

Carayol, A.: Regular sets of higher-order pushdown stacks. In: Jedrzejowicz, J., Szepietowski, A. (eds.) Mathematical Foundations of Computer Science, Proceedings of the 30th International Symposium, MFCS 2005, Gdansk, Poland, 29 August–2 September 2005. Lecture Notes in Computer Science, vol. 3618, pp. 168–179. Springer, Berlin (2005) CrossRef

10.

Carayol, A., Serre, O.: Collapsible pushdown automata and labeled recursion schemes: equivalence, safety and effective selection. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, 25–28 June 2012, pp. 165–174 (2012) CrossRef

11.

Carayol, A., Wöhrle, S.: The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003: Foundations of Software Technology and Theoretical Computer Science, Proceedings of the 23rd Conference, Mumbai, India, 15–17 December 2003. Lecture Notes in Computer Science, vol. 2914, pp. 112–123. Springer, Berlin (2003)

12.

Caucal, D.: On infinite transition graphs having a decidable monadic theory. Theor. Comput. Sci. 290(1), 79–115 (2003) MathSciNetCrossRefMATH

13.

Hague, M., Murawski, A.S., Ong, C.H.L., Serre, O.: Collapsible pushdown automata and recursion schemes. In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, Pittsburgh, PA, USA, 24–27 June 2008, pp. 452–461. IEEE Computer Society, Los Alamitos (2008) CrossRef

14.

Kartzow, A.: Collapsible pushdown graphs of level 2 are tree-automatic. Log. Methods Comput. Sci. 9(1) (2013)

15.

Kartzow, A., Parys, P.: Strictness of the collapsible pushdown hierarchy. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) Mathematical Foundations of Computer Science 2012, Proceedings of the 37th International Symposium, MFCS 2012, Bratislava, Slovakia, 27–31 August 2012. Lecture Notes in Computer Science, vol. 7464, pp. 566–577. Springer, Berlin (2012)

16.

Knapik, T., Niwinski, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) Foundations of Software Science and Computation Structures, Proceedings of the 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, 8–12 April 2002. Lecture Notes in Computer Science, vol. 2303, pp. 205–222. Springer, Berlin (2002)

17.

Knapik, T., Niwinski, D., Urzyczyn, P., Walukiewicz, I.: Unsafe grammars and panic automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) Automata, Languages and Programming, Proceedings of the 32nd International Colloquium, ICALP 2005, Lisbon, Portugal, 11–15 July 2005. Lecture Notes in Computer Science, vol. 3580, pp. 1450–1461. Springer, Berlin (2005)

18.

Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, 21–23 January 2009, pp. 416–428. ACM, New York (2009)

19.

Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983) MathSciNetCrossRefMATH

20.

Ong, C.H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26–28 January 2011. pp. 587–598. ACM, New York (2011)

21.

Parys, P.: Collapse operation increases expressive power of deterministic higher order pushdown automata. In: Schwentick, T., Dürr, C. (eds.) 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011, Dortmund, Germany, 10–12 March 2011. LIPIcs, vol. 9, pp. 603–614. Schloss Dagstuhl/Leibniz-Zentrum fuer Informatik, Berlin (2011)

22.

Parys, P.: On the significance of the collapse operation. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, 25–28 June 2012, pp. 521–530. IEEE, New York (2012) CrossRef

23.

Post, E.L.: A variant of a recursively unsolvable problem. J. Symb. Log. 12(2), 255–256 (1946)

24.

Trachtenbrot, B.: Impossibility of an algorithm for the decision problem on finite classes. Dokl. Akad. Nauk SSSR 70(70), 569–572 (1950) MATH

Titel: On First-Order Logic and CPDA Graphs
verfasst von: Christopher H. Broadbent
Publikationsdatum: 01.11.2014
Verlag: Springer US
Erschienen in: Theory of Computing Systems / Ausgabe 4/2014
Print ISSN: 1432-4350
Elektronische ISSN: 1433-0490
DOI: https://doi.org/10.1007/s00224-014-9533-0

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2014

Playing Mastermind with Constant-Size Memory

Model-Theoretic Properties of ω-Automatic Structures

The Complexity of Compressed Membership Problems for Finite Automata

Efficient Algorithms for Highly Compressed Data: The Word Problem in Generalized Higman Groups Is in P

Linear-Space Data Structures for Range Mode Query in Arrays

-Approximation for Graphic TSP

Premium Partner