Document Open Access Logo

Ordered Tree-Pushdown Systems

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2015.163.pdf
  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • reachability analysis
  • saturation technique
  • pushdown automata
  • ordered pushdown automata
  • higher-order pushdown automata
  • higher-order recursive sche

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Lorenzo Clemente, Pawel Parys, Sylvain Salvati, and Igor Walukiewicz. Ordered Tree-Pushdown Systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 163-177, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.FSTTCS.2015.163

Author Details

Lorenzo Clemente
Pawel Parys
Sylvain Salvati
Igor Walukiewicz

References

  1. K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Log. Methods Comput. Sci., 3(1):1-23, 2007. Google Scholar
  2. M. Atig. Model-checking of ordered multi-pushdown automata. Log. Methods Comput. Sci., 8(3), 09 2012. Google Scholar
  3. M. Atig, B. Bollig, and P. Habermehl. Emptiness of multi-pushdown automata is 2ETIME-complete. In Proc. of DLT'08, pages 121-133. Springer, 2008. Google Scholar
  4. W. Blum and C.-H. L. Ong. The safe lambda calculus. Log. Methods Comput. Sci., 5(1), 2009. Google Scholar
  5. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking and saturation method. In Proc. of CONCUR'97, volume 1243 of LNCS, pages 135-150, 1997. Google Scholar
  6. L. Breveglieri, A. Cherubini, C. Citrini, and S. Crespi-Reghizzi. Multi-push-down languages and grammars. Int. J. Found. Comput. Sci., 7(3):253-292, 1996. Google Scholar
  7. C. Broadbent, A. Carayol, M. Hague, and O. Serre. A saturation method for collapsible pushdown systems. In Proc. of ICALP'12, volume 7392 of LNCS, pages 165-176, 2012. Google Scholar
  8. C. Broadbent, A. Carayol, M. Hague, and O. Serre. C-SHORe: A collapsible approach to higher-order verification. In Proc. of ICFP '13, pages 13-24. ACM, 2013. Google Scholar
  9. C. Broadbent and N. Kobayashi. Saturation-based model checking of higher-order recursion schemes. In In Proc. of CSL'13, pages 129-148, 2013. Google Scholar
  10. A. Carayol and M. Hague. Saturation algorithms for model-checking pushdown systems. In Proc. of AFL'14, volume 151 of EPTCS, pages 1-24, 5 2014. Google Scholar
  11. L. Clemente, P. Parys, S. Salvati, and I. Walukiewicz. Ordered tree-pushdown systems. Technical report, University of Warsaw, October 2015. URL: http://arxiv.org/abs/1510.03278.
  12. A. Cyriac, P. Gastin, and K. Narayan Kumar. MSO decidability of multi-pushdown systems via split-width. In In Proc. of CONCUR'12, pages 547-561, 2012. Google Scholar
  13. J. Esparza and S. Schwoon. A BDD-based model checker for recursive programs. In Proc. of CAV'01, pages 324-336. Springer-Verlag, 2001. Google Scholar
  14. A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In Proc. of INFINITY'97, volume 9, pages 27-37, 1997. Google Scholar
  15. I. Guessarian. Pushdown tree automata. Theor. Comp. Sys., 16:237-263, 1983. Google Scholar
  16. Matthew H. Saturation of concurrent collapsible pushdown systems. In Proc. of FSTTCS'13, volume 24 of LIPIcs, pages 313-325, Dagstuhl, Germany, 2013. Google Scholar
  17. M. Hague, A. Murawski, C.-H. L. Ong, and O. Serre. Collapsible pushdown automata and recursion schemes. In Proc. of LICS'08, pages 452-461, 2008. Google Scholar
  18. M. Hague and C.-H. L. Ong. A saturation method for the modal mu-calculus over pushdown systems. Inform. and Comput., 209(5):799 - 821, May 2011. Google Scholar
  19. A. Kartzow and P. Parys. Strictness of the collapsible pushdown hierarchy. In Proc. of MFCS'12, pages 566-577. Springer, 2012. Google Scholar
  20. T. Knapik, D. Niwiński, and P. Urzyczyn. Higher-order pushdown trees are easy. In Proc. of FOSSACS'02, volume 2303 of LNCS, pages 205-222, 2002. Google Scholar
  21. T. Knapik, D. Niwiński, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. In Proc. of ICALP'05, pages 1450-1461. Springer-Verlag, 2005. Google Scholar
  22. J.-L. Krivine. A call-by-name lambda-calculus machine. Higher Order Symbol. Comput., 20:199-207, September 2007. Google Scholar
  23. A. Maslov. Multilevel stack automata. Probl. Peredachi Inf., 12(1):55-62, 1976. Google Scholar
  24. S. Salvati and I. Walukiewicz. Krivine machines and higher-order schemes. In Proc. of ICALP'11, volume 6756 of LNCS, pages 162-173. Springer-Verlag, 2011. Google Scholar
  25. S. Salvati and I. Walukiewicz. Krivine machines and higher-order schemes. Inf. Comput., 239(0):340-355, 2014. Google Scholar
  26. S. Salvati and I. Walukiewicz. Simply typed fixpoint calculus and collapsible pushdown automata. Math. Struct. in Comp. Science, pages 1-47, 5 2015. Google Scholar
  27. A. Seth. Global reachability in bounded phase multi-stack pushdown systems. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, Proc. of CAV'10, volume 6174 of LNCS, pages 615-628. Springer, 2010. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact