1 Search Results for "Broadbent, Christopher H."

Document
DOI: 10.4230/LIPIcs.STACS.2012.589
The Limits of Decidability for First Order Logic on CPDA Graphs

Authors: Christopher H. Broadbent

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

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.
Cite as

Christopher H. Broadbent. The Limits of Decidability for First Order Logic on CPDA Graphs. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 589-600, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{broadbent:LIPIcs.STACS.2012.589,
  author =	{Broadbent, Christopher H.},
  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 =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.589},
  URN =		{urn:nbn:de:0030-drops-34334},
  doi =		{10.4230/LIPIcs.STACS.2012.589},
  annote =	{Keywords: Collapsible Pushdown Automata, First Order Logic, Logical Reflection}
}
  • Refine by Author
  • 1 Broadbent, Christopher H.

  • Refine by Classification

  • Refine by Keyword
  • 1 Collapsible Pushdown Automata
  • 1 First Order Logic
  • 1 Logical Reflection

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2012

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact