Document Open Access Logo

Data Multi-Pushdown Automata

Authors Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.38.pdf
  • Filesize: 0.65 MB
  • 17 pages

Document Identifiers

Author Details

Parosh Aziz Abdulla
C. Aiswarya
Mohamed Faouzi Atig

Cite As Get BibTex

Parosh Aziz Abdulla, C. Aiswarya, and Mohamed Faouzi Atig. Data Multi-Pushdown Automata. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.38

Abstract

We extend the classical model of multi-pushdown systems by considering systems that operate on a finite set of variables ranging over natural numbers. The conditions on variables are defined via gap-order constraints that allow to compare variables for equality, or to check that the gap between the values of two variables exceeds a given natural number. Furthermore, each message inside a stack is equipped with a data item representing its value. When a message is pushed to the stack, its value may be defined by a variable. When a message is popped, its value may be copied to a variable. Thus, we obtain a system that is infinite in multiple dimensions, namely we have a number of stacks that may contain an unbounded number of messages each of which is equipped with a natural number. 
It is well-known that the verification of any non-trivial property of multi-pushdown systems is undecidable, even for two stacks and for a finite data-domain. In this paper, we show the decidability of the reachability problem for the classes of data multi-pushdown system that admit a bounded split-width (or equivalently a bounded tree-width). As an immediate consequence, we obtain decidability for several subclasses of data multi-pushdown systems. These include systems with single stacks, restricted ordering policies on stack operations, bounded scope, bounded phase, and bounded context switches.

Subject Classification

Keywords
  • Pushdown Systems
  • Model-Checking
  • Gap-Order
  • Bounded Split-Width

Metrics

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

References

  1. P. A. Abdulla, M. F. Atig, G. Delzanno, and A. Podelski. Push-down automata with gap-order constraints. In FSEN, volume 8161 of LNCS, pages 199-216. Springer, 2013. Google Scholar
  2. P. A. Abdulla, M. F. Atig, O. Rezine, and J.Stenman. Budget-bounded model-checking pushdown systems. Formal Methods in System Design, 45(2):273-301, 2014. Google Scholar
  3. P. A. Abdulla, M. F. Atig, and J. Stenman. The minimal cost reachability problem in priced timed pushdown systems. In LATA, volume 7183 of LNCS, 2012. Google Scholar
  4. P. A. Abdulla and G. Delzanno. On the coverability problem for constrained multiset rewriting. In Proc. AVIS'06, The fifth Int. Workshop on on Automated Verification of Infinite-State Systems, 2006. Google Scholar
  5. C. Aiswarya, P Gastin, and K. Narayan Kumar. Controllers for the verification of communicating multi-pushdown systems. In CONCUR, volume 8704 of LNCS, pages 297-311, 2014. Google Scholar
  6. C. Aiswarya, P. Gastin, and K. Narayan Kumar. Verifying communicating multi-pushdown systems via split-width. In ATVA'14, volume 8837 of LNCS. Springer, 2014. To appear. Google Scholar
  7. S. Akshay, P. Gastin, V. Juge, and S. N. Krishna. personal communication. Google Scholar
  8. S. Akshay, P. Gastin, and S. N. Krishna. Analyzing timed systems using tree automata. In CONCUR'16, volume 59 of LIPICS, pages 27:1-27:14. Leibniz-Zentrum für Informatik, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.27.
  9. M. F. Atig. Global Model Checking of Ordered Multi-Pushdown Systems. In FSTTCS 2010, volume 8, pages 216-227, 2010. Google Scholar
  10. M. F. Atig, B. Bollig, and P. Habermehl. Emptiness of multi-pushdown automata is 2ETIME-complete. In Proceedings of DLT'08, volume 5257 of LNCS, pages 121-133. Springer, 2008. Google Scholar
  11. M. F. Atig, K. Narayan Kumar, and P. Saivasan. Adjacent ordered multi-pushdown systems. Int. J. Found. Comput. Sci., 25(8):1083-1096, 2014. Google Scholar
  12. M. F. Atig, K. Narayan Kumar, and P. Saivasan. Acceleration in multi-pushdown systems. In TACAS 2016, volume 9636 of LNCS, pages 698-714. Springer, 2016. Google Scholar
  13. Mohamed Faouzi Atig. Model-checking of ordered multi-pushdown automata. Logical Methods in Computer Science, 8(3), 2012. Google Scholar
  14. B. Bollig, A. Cyriac, P. Gastin, and K. Narayan Kumar. Model checking languages of data words. In FoSSaCS'12, volume 7213 of LNCS, pages 391-405. Springer, March 2012. Google Scholar
  15. A. Bouajjani, R. Echahed, and R. Robbana. On the automatic verification of systems with continuous variables and unbounded discrete data structures. In Hybrid Systems II, volume 999 of LNCS, pages 64-85. Springer, 1994. Google Scholar
  16. L. Breveglieri, A. Cherubini, C. Citrini, and S. Crespi Reghizzi. Multi-push-down languages and grammars. International Journal of Foundations of Computer Science, 7(3):253-292, 1996. Google Scholar
  17. X. Cai and M. Ogawa. Well-structured pushdown systems. In CONCUR 2013, volume 8052 of LNCS, pages 121-136. Springer, 2013. Google Scholar
  18. K. Čerāns. Deciding properties of integral relational automata. In Abiteboul and Shamir, editors, ICALP 94, volume 820 of LNCS, pages 35-46. Springer Verlag, 1994. Google Scholar
  19. Lorenzo Clemente and Slawomir Lasota. Reachability analysis of first-order definable pushdown systems. In CSL 2015,, volume 41 of LIPIcs, pages 244-259. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  20. B. Courcelle. The expression of graph properties and graph transformations in monadic second-order logic. In Grzegorz Rozenberg, editor, Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, pages 313-400. World Scientific, 1997. Google Scholar
  21. A. Cyriac, P. Gastin, and K. Narayan Kumar. MSO decidability of multi-pushdown systems via split-width. In CONCUR'12, volume 7454 of LNCS, pages 547-561. Springer, 2012. Google Scholar
  22. F. S. de Boer, M. M. Bonsangue, and J. Rot. It is pointless to point in bounded heaps. Sci. Comput. Program., 112:102-118, 2015. Google Scholar
  23. M. Fortin and P. Gastin. Verification of parameterized communicating automata via split-width. In FoSSaCS'16, volume 9634 of LNCS, pages 197-213. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49630-5_12.
  24. A. Heußner, J. Leroux, A. Muscholl, and G. Sutre. Reachability analysis of communicating pushdown systems. Logical Methods in Computer Science, 8(3), 2012. URL: http://dx.doi.org/10.2168/LMCS-8(3:23)2012.
  25. S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In LICS'07, pages 161-170. IEEE Computer Society Press, 2007. Google Scholar
  26. S. La Torre and M. Napoli. Reachability of multistack pushdown systems with scope-bounded matching relations. In CONCUR 2011, volume 6901 of LNCS, pages 203-218. Springer, 2011. Google Scholar
  27. S. La Torre and G. Parlato. Scope-bounded multistack pushdown systems: Fixed-point, sequentialization, and tree-width. In FSTTCS 2012, volume 18 of LIPIcs, pages 173-184. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  28. A. Lal and T.W. Reps. Reducing concurrent analysis under a context bound to sequential analysis. In CAV, volume 5123 of LNCS, pages 37-51. Springer, 2008. Google Scholar
  29. P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In Thomas Ball and Mooly Sagiv, editors, POPL, pages 283-294. ACM, 2011. Google Scholar
  30. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In N. Halbwachs and L.D. Zuck, editors, TACAS 2005, volume 3440 of LNCS, pages 93-107. Springer, 2005. Google Scholar
  31. G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst., 22(2):416-430, 2000. Google Scholar
  32. P. Revesz. A closed form evaluation for datalog queries with integer (gap)-order constraints. Theoretical Computer Science, 116(1):117-149, 1993. Google Scholar
  33. A. Seth. Global reachability in bounded phase multi-stack pushdown systems. In CAV'10, LNCS, 2010. Google Scholar
  34. S. La Torre, P. Madhusudan, and G. Parlato. Reducing context-bounded concurrent reachability to sequential reachability. In CAV, volume 5643 of LNCS, pages 477-492. Springer, 2009. 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