2026-07-23T03:28:45Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5647 2024-03-06T10:36:43Z ddc:004 open_access

Ordered Tree-Pushdown Systems Clemente, Lorenzo Parys, Pawel Salvati, Sylvain Walukiewicz, Igor reachability analysis saturation technique pushdown automata ordered pushdown automata higher-order pushdown automata higher-order recursive sche 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lorenzo Clemente and Pawel Parys and Sylvain Salvati and Igor Walukiewicz 2015 Is Part Of LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2015.163 urn:nbn:de:0030-drops-56470 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.163 eng https://creativecommons.org/licenses/by/3.0/legalcode