License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2015.163
URN: urn:nbn:de:0030-drops-56470
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5647/
Go to the corresponding LIPIcs Volume Portal

Clemente, Lorenzo ; Parys, Pawel ; Salvati, Sylvain ; Walukiewicz, Igor

Ordered Tree-Pushdown Systems

pdf-format:
33.pdf (0.5 MB)

Abstract

We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering restriction, and we show that the resulting class enjoys a decidable reachability problem. This follows from a preservation of recognizability result for the backward reachability relation of such systems. As an application, we show that our simple model can encode several formalisms generalizing pushdown systems, such as ordered multi-pushdown systems, annotated higher-order pushdown systems, the Krivine machine, and ordered annotated multi-pushdown systems. In each case, our procedure yields tight complexity.

BibTeX - Entry

@InProceedings{clemente_et_al:LIPIcs:2015:5647,
  author =	{Lorenzo Clemente and Pawel Parys and Sylvain Salvati and Igor Walukiewicz},
  title =	{{Ordered Tree-Pushdown Systems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{163--177},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Prahladh Harsha and G. Ramalingam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5647},
  URN =		{urn:nbn:de:0030-drops-56470},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.163},
  annote =	{Keywords: reachability analysis, saturation technique, pushdown automata, ordered pushdown automata, higher-order pushdown automata, higher-order recursive sche}
}

Keywords: reachability analysis, saturation technique, pushdown automata, ordered pushdown automata, higher-order pushdown automata, higher-order recursive sche
Collection: 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)
Issue Date: 2015
Date of publication: 14.12.2015

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