Document Open Access Logo

On the Complexity of Multi-Pushdown Games

Authors Roland Meyer, Sören van der Wall

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.52.pdf
  • Filesize: 0.69 MB
  • 35 pages

Document Identifiers

Author Details

Roland Meyer
  • TU Braunschweig, Germany
Sören van der Wall
  • TU Braunschweig, Germany

Funding

This work was partially supported by DFG grant 417532197 Effective Denotational Semantics for Synthesis (EDS@SYN).

Cite AsGet BibTex

Roland Meyer and Sören van der Wall. On the Complexity of Multi-Pushdown Games. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 52:1-52:35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSTTCS.2020.52

Abstract

We study the influence of parameters like the number of contexts, phases, and stacks on the complexity of solving parity games over concurrent recursive programs. Our first result shows that k-context games are b-EXPTIME-complete, where b = max{k-2, 1}. This means up to three contexts do not increase the complexity over an analysis for the sequential case. Our second result shows that for ordered k-stack as well as k-phase games the complexity jumps to k-EXPTIME-complete.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • concurrency
  • complexity
  • games
  • infinite state
  • multi-pushdown

Metrics

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

References

  1. CPAchecker. URL: https://cpachecker.sosy-lab.org/index.php.
  2. ULTIMATE Automizer and ULTIMATE Taipan. URL: https://monteverdi.informatik.uni-freiburg.de/tomcat/Website/.
  3. K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. LMCS, 3(3), 2007. Google Scholar
  4. S. Akshay, P. Gastin, S. Krishna, and S. Roychowdhury. Revisiting underapproximate reachability for multipushdown systems. In TACAS, volume 12078 of LNCS, pages 387-404. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_21.
  5. M. F. Atig. From multi to single stack automata. In CONCUR, volume 6269 of LNCS, pages 117-131. Springer, 2010. Google Scholar
  6. M. F. Atig. Global model checking of ordered multi-pushdown systems. In FSTTCS, volume 8 of LIPIcs, pages 216-227. Dagstuhl, 2010. Google Scholar
  7. M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan. Model checking branching-time properties of multi-pushdown systems is hard. CoRR, abs/1205.6928, 2012. URL: http://arxiv.org/abs/1205.6928.
  8. M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan. Parity games on bounded phase multi-pushdown systems. In NETYS, volume 10299 of LNCS, pages 272-287. Springer, 2017. Google Scholar
  9. T. A. Beyene, S. Chaudhuri, C. Popeea, and A. Rybalchenko. A constraint-based approach to solving games on infinite graphs. In POPL, pages 221-234. ACM, 2014. Google Scholar
  10. T. A. Beyene, S. Chaudhuri, C. Popeea, and A. Rybalchenko. Recursive games for compositional program synthesis. In VSTTE, volume 9593 of LNCS, pages 19-39. Springer, 2015. Google Scholar
  11. D. Beyer. Advances in automatic software verification: SV-COMP 2020. In TACAS, volume 12079 of LNCS, pages 347-367. Springer, 2020. Google Scholar
  12. D. Beyer, M. Dangl, and P. Wendler. A unifying view on SMT-based software verification. JAR, 60(3):299-335, 2018. Google Scholar
  13. D. Beyer and M. E. Keremoglu. CPAchecker: A tool for configurable software verification. In Proc. CAV, volume 6806 of LNCS, pages 184-190. Springer, 2011. Google Scholar
  14. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, volume 1243 of LNCS, pages 135-150. Springer, 1997. Google Scholar
  15. A. Bouajjani and A. Meyer. Symbolic reachability analysis of higher-order context-free processes. In FSTTCS, volume 3328 of LNCS, pages 135-147. Springer, 2004. Google Scholar
  16. 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
  17. C. H. Broadbent, A. Carayol, M. Hague, and O. Serre. A saturation method for collapsible pushdown systems. In ICALP, volume 7392 of LNCS, pages 165-176. Springer, 2012. Google Scholar
  18. C. H. Broadbent, A. Carayol, M. Hague, and O. Serre. C-SHORe: a collapsible approach to higher-order verification. In ICFP, pages 13-24. ACM, 2013. Google Scholar
  19. C. H. Broadbent and N. Kobayashi. Saturation-based model checking of higher-order recursion schemes. In CSL, volume 23 of LIPIcs, pages 129-148. Dagstuhl, 2013. Google Scholar
  20. J. R. Büchi. Regular canonical systems. Archiv für mathematische Logik und Grundlagenforschung, 6(3):91-111, 1964. Google Scholar
  21. T. Cathcart Burn, C.-H. L. Ong, and S. J. Ramsay. Higher-order constrained Horn clauses for verification. Proc. ACM Program. Lang., 2(POPL):11:1-11:28, 2018. Google Scholar
  22. Aiswarya C. Verification of communicating recursive programs via split-width. PhD thesis, ENS Cachan, 2014. Google Scholar
  23. T. Cachat. Symbolic strategy synthesis for games on pushdown graphs. In ICALP, volume 2380 of LNCS, pages 704-715. Springer, 2002. Google Scholar
  24. T. Cachat and I. Walukiewicz. The complexity of games on higher order pushdown automata. CoRR, abs/0705.0262, 2007. URL: http://arxiv.org/abs/0705.0262.
  25. A. Carayol and M. Hague. Saturation algorithms for model-checking pushdown systems. In AFL, volume 151 of EPTCS, pages 1-24, 2014. Google Scholar
  26. A. Carayol, M. Hague, A. Meyer, C.-H. L. Ong, and O. Serre. Winning regions of higher-order pushdown games. In LICS, pages 193-204. IEEE, 2008. Google Scholar
  27. A. K. Chandra, D. C. Kozen, and L. J. Stockmeyer. Alternation. JACM, 28(1):114-133, 1981. Google Scholar
  28. B. Courcelle and J. Engelfriet. Graph Structure and Monadic Second-Order Logic. CUP, 2012. Google Scholar
  29. A. Cyriac, P. Gastin, and K. N. Kumar. MSO decidability of multi-pushdown systems via split-width. In CONCUR, volume 7454 of LNCS, pages 547-561. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32940-1_38.
  30. H. B. Enderton. A mathematical introduction to logic. Academic Press, 1972. Google Scholar
  31. J. Esparza. On the decidability of model checking for several μ-calculi and Petri nets. In CAAP, volume 787 of LNCS, pages 115-129. Springer, 1994. Google Scholar
  32. A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. In Infinity, volume 9 of ENTCS, pages 27-37. Elsevier, 1997. Google Scholar
  33. E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games, volume 2500 of LNCS. Springer, 2002. Google Scholar
  34. C. Grellois and P.-A. Melliès. Finitary semantics of linear logic and higher-order model-checking. In MFCS, volume 9234 of LNCS, pages 256-268. Springer, 2015. Google Scholar
  35. M. Hague. Saturation of concurrent collapsible pushdown systems. In FSTTCS, volume 24 of LIPIcs, pages 313-325. Dagstuhl, 2013. Google Scholar
  36. M. Hague, R. Meyer, and S. Muskalla. Domains for Higher-Order Games. In MFCS, volume 83 of LIPIcs, pages 59:1-59:15. Dagstuhl, 2017. Google Scholar
  37. M. Hague and C.-H. L. Ong. Symbolic backwards-reachability analysis for higher-order pushdown systems. LMCS, 4(4), 2008. Google Scholar
  38. M. Heizmann, Y.-W. Chen, D. Dietsch, M. Greitschus, A. Nutz, B. Musa, C. Schätzle, C. Schilling, F. Schüssele, and Andreas Podelski. Ultimate Automizer with an on-demand construction of Floyd-Hoare automata. In TACAS, volume 10206 of LNCS, pages 394-398. Springer, 2017. Google Scholar
  39. M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL, pages 471-482. ACM, 2010. Google Scholar
  40. T. A. Henzinger. Games in system design and verification. In TARK, pages 1-4. National University of Singapore, 2005. Google Scholar
  41. M. Hofmann and J. Ledent. A cartesian-closed category for higher-order model checking. In LICS, pages 1-12. IEEE, 2017. Google Scholar
  42. M. Jurdzinski. Small progress measures for solving parity games. In STACS, volume 1770 of LNCS, pages 290-301. Springer, 2000. URL: https://doi.org/10.1007/3-540-46541-3.
  43. M. Jurdzinski and R. Lazic. Succinct progress measures for solving parity games. In LICS, pages 1-9. IEEE, 2017. Google Scholar
  44. M. Jurdzinski, M. Paterson, and U. Zwick. A deterministic subexponential algorithm for solving parity games. SIAM J. C., 38(4):1519-1532, 2008. Google Scholar
  45. N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, pages 416-428. ACM, 2009. Google Scholar
  46. N. Kobayashi and C.-H. L. Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In LICS, pages 179-188. IEEE, 2009. Google Scholar
  47. S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In LICS, pages 161-170. IEEE, 2007. Google Scholar
  48. S. La Torre, P. Madhusudan, and G. Parlato. Model-checking parameterized concurrent programs using linear interfaces. In CAV, volume 6174 of LNCS, pages 629-644. Springer, 2010. Google Scholar
  49. S. La Torre and M. Napoli. Reachability of multistack pushdown systems with scope-bounded matching relations. In CONCUR, volume 6901 of LNCS, pages 203-218. Springer, 2011. Google Scholar
  50. P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL, pages 283-294. ACM, 2011. Google Scholar
  51. C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81-90. IEEE, 2006. Google Scholar
  52. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, volume 3440 of LNCS, pages 93-107. Springer, 2005. Google Scholar
  53. G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. ACM ToPLaS, 22(2):416-430, 2000. Google Scholar
  54. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, pages 49-61. ACM, 1995. Google Scholar
  55. S. Salvati and I. Walukiewicz. A model for behavioural properties of higher-order programs. In CSL, volume 41 of LIPIcs, pages 229-243. Dagstuhl, 2015. Google Scholar
  56. A. Seth. Games on higher order multi-stack pushdown systems. In RP, volume 5797 of LNCS, pages 203-216. Springer, 2009. Google Scholar
  57. A. Seth. Games on multi-stack pushdown systems. In LFCS, volume 5407 of LNCS, pages 395-408. Springer, 2009. Google Scholar
  58. M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. TR 2, NYU, 1978. Google Scholar
  59. L. J. Stockmeyer. The complexity of decision problems in automata theory and logic. PhD thesis, MIT, 1974. Google Scholar
  60. S. van der Wall. Bounded analysis of concurrent and recursive programs. Master’s thesis, TU Braunschweig, 2019. URL: http://www.tcs.cs.tu-bs.de/documents/thesis-van-der-wall-2019.pdf.
  61. I. Walukiewicz. Pushdown processes: games and model-checking. IC, 164(2):234-263, 2001. Google Scholar
  62. I. Walukiewicz. A landscape with games in the background. In LICS, pages 356-366. IEEE, 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 Imprint Privacy Contact