License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2012.589
URN: urn:nbn:de:0030-drops-34334
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3433/
Go to the corresponding LIPIcs Volume Portal

Broadbent, Christopher H.

The Limits of Decidability for First Order Logic on CPDA Graphs

pdf-format:
49.pdf (0.7 MB)

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 lambda-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 [Kartzow 2010] 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.

BibTeX - Entry

@InProceedings{broadbent:LIPIcs:2012:3433,
  author =	{Christopher H. Broadbent},
  title =	{{The Limits of Decidability for First Order Logic on CPDA Graphs}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{589--600},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{Christoph D{\"u}rr and Thomas Wilke},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3433},
  URN =		{urn:nbn:de:0030-drops-34334},
  doi =		{10.4230/LIPIcs.STACS.2012.589},
  annote =	{Keywords: Collapsible Pushdown Automata, First Order Logic, Logical Reflection}
}

Keywords: Collapsible Pushdown Automata, First Order Logic, Logical Reflection
Collection: 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)
Issue Date: 2012
Date of publication: 24.02.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI