Document Open Access Logo

Reachability Analysis of First-order Definable Pushdown Systems

Authors Lorenzo Clemente, Slawomir Lasota

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.244.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Lorenzo Clemente
Slawomir Lasota

Cite As Get BibTex

Lorenzo Clemente and Slawomir Lasota. Reachability Analysis of First-order Definable Pushdown Systems. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 244-259, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.244

Abstract

We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are first-order definable in a fixed countably-infinite structure. We show that the reachability analysis can be addressed with the well-known saturation technique for the wide class of oligomorphic structures. Moreover, for the more restrictive homogeneous structures, we are able to give concrete complexity upper bounds. We show ample applicability of our technique by presenting several concrete examples of homogeneous structures, subsuming, with optimal complexity, known results from the literature. We show that infinitely many such examples of homogeneous structures can be obtained with the classical wreath product construction.

Subject Classification

Keywords
  • automata theory
  • pushdown systems
  • sets with atoms
  • saturation technique

Metrics

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

References

  1. P. A. Abdulla, M. F. Atig, and J. Stenman. Dense-timed pushdown automata. In Proc. of LICS'12, pages 35-44, june 2012. Google Scholar
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. Timed lossy channel systems. In Proc. of FSTTCS'12, volume 18 of LIPIcs, pages 374-386, 2012. Google Scholar
  3. Parosh Aziz Abdulla and Aletta Nylén. Timed Petri nets and BQOs. In Proc. of ICATPN'01, pages 53-70, 2001. Google Scholar
  4. Mohamed F. Atig. Model-checking of ordered multi-pushdown automata. Log. Methods Comput. Sci., 8(3), 09 2012. Google Scholar
  5. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Logical Methods in Computer Science, 10(3:4):paper 4, 2014. Google Scholar
  6. Benedikt Bollig, Aiswarya Cyriac, Paul Gastin, and K. Narayan Kumar. Model checking languages of data words. In Lars Birkedal, editor, Proc. of FOSSACS'12, volume 7213 of LNCS, pages 391-405. Springer, 2012. Google Scholar
  7. Ahmed Bouajjani, Javier Esparza, and Oded 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
  8. Ahmed Bouajjani, Peter Habermehl, Yan Jurski, and Mihaela Sighireanu. Rewriting systems with data. In In Proc. of FCT'07, volume 4639 of LNCS, pages 1-22. Springer, 2007. Google Scholar
  9. Luca Breveglieri, Alessandra Cherubini, Claudio Citrini, and Stefano Crespi-Reghizzi. Multi-push-down languages and grammars. Int. J. Found. Comput. Sci., 7(3):253-292, 1996. Google Scholar
  10. Chris Broadbent, Arnaud Carayol, Matthew Hague, and Olivier Serre. A saturation method for collapsible pushdown systems. In Proc. of ICALP'12, volume 7392 of LNCS, pages 165-176, 2012. Google Scholar
  11. Arnaud Carayol and Matthew Hague. Saturation algorithms for model-checking pushdown systems. In Proc. of AFL'14, volume 151 of EPTCS, pages 1-24, 5 2014. Google Scholar
  12. Edward Y. C. Cheng and Michael Kaminski. Context-free languages over infinite alphabets. Acta Inf., 35(3):245-267, 1998. Google Scholar
  13. L. Clemente and S. Lasota. Timed pushdown automata revisited. In Proc. of LICS'15, 2015. Accepted for publication. Google Scholar
  14. Wojciech Czerwiński, Piotr Hofman, and Sławomir Lasota. Reachability problem for weak multi-pushdown automata. Logical Methods in Computer Science, 9(3:13):1-29, 2013. Google Scholar
  15. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Logic, 10(3):16:1-16:30, April 2009. Google Scholar
  16. Alin Deutsch, Richard Hull, Fabio Patrizi, and Victor Vianu. Automatic verification of data-centric business processes. In Proc. of ICDT'09, pages 252-267, New York, NY, USA, 2009. ACM. Google Scholar
  17. Javier Esparza and Stefan Schwoon. A BDD-based model checker for recursive programs. In Proc. of CAV'01, CAV'01, pages 324-336. Springer-Verlag, 2001. Google Scholar
  18. Alain Finkel, Bernard Willems, and Pierre Wolper. A direct symbolic approach to model checking pushdown systems. In Proc. of INFINITY'97, volume 9, pages 27-37, 1997. Google Scholar
  19. R. Fraïssé. Theory of relations. North-Holland, 1953. Google Scholar
  20. Irène Guessarian. Pushdown tree automata. Theor. Comp. Sys., 16:237-263, 1983. Google Scholar
  21. Ward Henson. Countable homogeneous relational structures and ℵ₀-categorical theories. J. Symb. Logic, 37:494–500, 1972. Google Scholar
  22. Slawomir Lasota and Igor Walukiewicz. Alternating timed automata. ACM Trans. Comput. Logic, 9(2):10:1-10:27, 2008. Google Scholar
  23. Ranko Lazic, Tom Newcomb, Joël Ouaknine, A. W. Roscoe, and James Worrell. Nets with tokens which carry data. In Proc. of ICATPN'07, LNCS, pages 301-320. Springer-Verlag, 2007. Google Scholar
  24. Dugald Macpherson. A survey of homogeneous structures. Discrete Mathematics, 311(15):1599–1634, 2011. Google Scholar
  25. A. N. Maslov. Multilevel stack automata. Probl. Peredachi Inf., 12(1):55-62, 1976. Google Scholar
  26. Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. Reachability in pushdown register automata. In MFCS 2014, pages 464-473, 2014. Google Scholar
  27. Joel Ouaknine and James Worrell. On the language inclusion problem for timed automata: Closing a decidability gap. In In Proc. of LICS'04, pages 54-63. IEEE Computer Society, 2004. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact