Document Open Access Logo

Summaries for Context-Free Games

Authors Lukás Holík, Roland Meyer, Sebastian Muskalla

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.41.pdf
  • Filesize: 0.54 MB
  • 16 pages

Document Identifiers

Author Details

Lukás Holík
Roland Meyer
Sebastian Muskalla

Cite As Get BibTex

Lukás Holík, Roland Meyer, and Sebastian Muskalla. Summaries for Context-Free Games. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 41:1-41:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSTTCS.2016.41

Abstract

We study two-player games played on the infinite graph of sentential forms induced by a context-free grammar (that comes with an ownership partitioning of the non-terminals). The winning condition is inclusion of the derived terminal word in the language of a finite automaton. Our contribution is a new algorithm to decide the winning player and to compute her strategy. It is based on a novel representation of all plays starting in a non-terminal. The representation uses the domain of Boolean formulas over the transition monoid of the target automaton. The elements of the monoid are essentially procedure summaries, and our approach can be seen as the first summary-based algorithm for the synthesis of recursive programs. We show that our algorithm has optimal (doubly exponential) time complexity, that it is compatible with recent antichain optimizations, and that it admits a lazy evaluation strategy. Our preliminary experiments indeed show encouraging results, indicating a speed up of three orders of magnitude over a competitor.

Subject Classification

Keywords
  • summaries
  • context-free games
  • Kleene iteration
  • transition monoid
  • strategy synthesis

Metrics

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

References

  1. Implementation of our algorithm. Published: 2016-17-07. URL: https://concurrency.informatik.uni-kl.de/rigg.html.
  2. P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. In LICS, pages 313-321, 1996. Google Scholar
  3. P. A. Abdulla, Y. Chen, L. Clemente, L. Holík, C.-D. Hong, R. Mayr, and T. Vojnar. Simulation subsumption in Ramsey-based Büchi automata universality and inclusion testing. In CAV, volume 6174 of LNCS, pages 132-147. Springer, 2010. Google Scholar
  4. P. A. Abdulla, Y. Chen, L. Clemente, L. Holík, C.-D. Hong, R. Mayr, and T. Vojnar. Advanced Ramsey-based Büchi automata inclusion testing. In CONCUR, volume 6901 of LNCS, pages 187-202. Springer, 2011. Google Scholar
  5. P. A. Abdulla, F. Haziza, and L. Holík. All for the price of few. In VMCAI, volume 7737 of LNCS, pages 476-495. Springer, 2013. Google Scholar
  6. D. Beyer. Software verification and verifiable witnesses (report on sv-comp). In TACAS, volume 9035 of LNCS, pages 401-416. Springer, 2015. Google Scholar
  7. D. Beyer. Reliable and reproducible competition results with benchexec and witnesses (report on sv-comp). In TACAS, volume 9636 of LNCS, pages 887-904. Springer, 2016. Google Scholar
  8. H. Björklund, M. Schuster, T. Schwentick, and J. Kulbatzki. On optimum left-to-right strategies for active context-free games. In ICDT, pages 105-116. ACM, 2013. Google Scholar
  9. 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
  10. C. Broadbent, A. Carayol, M. Hague, and Olivier O. Serre. C-SHORe: A collapsible approach to higher-order verification. ACM SIGPLAN Notices, 48(9):13-24, 2013. Google Scholar
  11. C. 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
  12. J. R. Büchi. On a Decision Method in Restricted Second Order Arithmetic, pages 425-435. Springer, 1990. Google Scholar
  13. T. Cachat. Symbolic strategy synthesis for games on pushdown graphs. In ICALP, volume 2380 of LNCS, pages 704-715. Springer, 2002. Google Scholar
  14. A. Carayol and M. Hague. Saturation algorithms for model-checking pushdown systems. In AFL, volume 151 of EPTCS, pages 1-24, 2014. Google Scholar
  15. B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. CUP, 1990. Google Scholar
  16. J. Esparza, S. Kiefer, and M. Luttenberger. Newtonian program analysis. JACM, 57(6), 2010. Google Scholar
  17. J. Fiedor, L. Holík, P. Jank\ou, O. Lengál, and T. Vojnar. Lazy automata techniques for WS1S. Technical Report FIT-TR-2016-01, Brno University of Technology, 2016. Google Scholar
  18. A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. ENTCS, 9:27-37, 1997. Google Scholar
  19. S. Fogarty and M. Y. Vardi. Efficient Büchi universality checking. In TACAS, volume 6015 of LNCS, pages 205-220. Springer, 2010. Google Scholar
  20. Z. Ganjei, A. Rezine, P. Eles, and Z. Peng. Lazy constrained monotonic abstraction. In VMCAI, volume 9583 of LNCS, pages 147-165. Springer, 2016. Google Scholar
  21. P. Ganty, J.-F. Raskin, and L. Begin. A complete abstract interpretation framework for coverability properties of WSTS. In VMCAI, pages 49-64. Springer, 2006. Google Scholar
  22. M. Hague and C.-H. L. Ong. Winning regions of pushdown parity games: A saturation method. In CONCUR, volume 5710 of LNCS, pages 384-398. Springer, 2009. Google Scholar
  23. M. Hague and C.-H. L. Ong. Analysing mu-calculus properties of pushdown systems. In SPIN, volume 6349 of LNCS, pages 187-192. Springer, 2010. Google Scholar
  24. M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL, pages 471-482. ACM, 2010. Google Scholar
  25. L. Holík, R. Meyer, and S. Muskalla. Summaries for context-free games. CoRR, abs/1603.07256, 2016. URL: http://arxiv.org/abs/1603.07256.
  26. A. Kaiser, D. Kroening, and T. Wahl. Efficient coverability analysis by proof minimization. In CONCUR, pages 500-515. Springer, 2012. Google Scholar
  27. J. Kloos, R. Majumdar, F. Niksic, and R. Piskac. Incremental, inductive coverability. In CAV, volume 9206 of LNCS, pages 158-173. Springer, 2013. Google Scholar
  28. O. Kupferman, N. Piterman, and M. Y. Vardi. An automata-theoretic approach to infinite-state systems. In Time for Verification: Essays in Memory of Amir Pnueli, volume 6200 of LNCS, pages 202-259. Springer, 2010. Google Scholar
  29. Z. Long, G. Calin, R. Majumdar, and R. Meyer. Language-theoretic abstraction refinement. In FASE, volume 7212 of LNCS, pages 362-376. Springer, 2012. Google Scholar
  30. A. Muscholl, T. Schwentick, and L. Segoufin. Active context-free games. Theory of Computing Systems, 39(1):237-276, 2005. Google Scholar
  31. N. Piterman and M. Y. Vardi. Global model-checking of infinite-state systems. In CAV, volume 3114 of LNCS, pages 387-400. Springer, 2004. Google Scholar
  32. S. J. Ramsay, R. P. Neatherway, and C.-H. L. Ong. A type-directed abstraction refinement approach to higher-order model checking. In POPL, pages 61-72. ACM, 2014. Google Scholar
  33. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, pages 49-61. ACM, 1995. Google Scholar
  34. M. Schuster and T. Schwentick. Games for active XML revisited. In ICDT, volume 31 of LIPIcs, pages 60-75. Dagstuhl, 2015. Google Scholar
  35. S. Schwoon. Model-Checking Pushdown Systems. PhD thesis, TU Munich, 2002. Google Scholar
  36. O. Serre. Note on winning positions on pushdown games with omega-regular conditions. IPL, 85(6):285-291, 2003. Google Scholar
  37. M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. Technical Report 2, New York University, 1978. Google Scholar
  38. A. P. Sistla, M. Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with applications to temporal logic. In ICALP, volume 194 of LNCS, pages 217-237. Springer, 1985. Google Scholar
  39. D. Suwimonteerabuth, S. Schwoon, and J. Esparza. Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In ATVA, volume 4218 of LNCS, pages 141-153. Springer, 2006. Google Scholar
  40. D. Tabakov and M. Y. Vardi. Experimental evaluation of classical automata constructions. In LPAR, volume 3835 of LNCS, pages 396-411. Springer, 2005. Google Scholar
  41. WALi. Visited: 2016-16-07. URL: https://research.cs.wisc.edu/wpis/wpds/download.php.
  42. I. Walukiewicz. Pushdown processes: Games and model-checking. IC, 164(2):234-263, 2001. Google Scholar
  43. M. Wulf, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Antichains: A new algorithm for checking universality of finite automata. In CAV, volume 4144 of LNCS. Springer, 2006. Google Scholar
  44. M. De Wulf, L. Doyen, and J.-F. Raskin. A lattice theory for solving games of imperfect information. In HSCC, volume 3927 of LNCS, pages 153-168. Springer, 2006. 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