Document Open Access Logo

Domains for Higher-Order Games

Authors Matthew Hague, Roland Meyer, Sebastian Muskalla

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.59.pdf
  • Filesize: 0.51 MB
  • 15 pages

Document Identifiers

Author Details

Matthew Hague
Roland Meyer
Sebastian Muskalla

Cite AsGet BibTex

Matthew Hague, Roland Meyer, and Sebastian Muskalla. Domains for Higher-Order Games. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 59:1-59:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.MFCS.2017.59

Abstract

We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied.
Keywords
  • higher-order recursion schemes
  • games
  • semantics
  • abstract interpretation
  • fixed points

Metrics

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

References

  1. 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
  2. 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
  3. S. Abramsky. Abstract interpretation, logical relations and Kan extensions. J. Log. Comp., 1(1):5-40, 1990. Google Scholar
  4. S. Abramsky and C. Hankin. An introduction to abstract interpretation. In Abstract Interpretation of declarative languages, volume 1, pages 63-102. Ellis Horwood, 1987. Google Scholar
  5. K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. LMCS, 3(3):1-23, 2007. Google Scholar
  6. K. Backhouse and R. C. Backhouse. Safety of abstract interpretations for free, via logical relations and Galois connections. Sci. Comp. Prog., 51(1-2):153-196, 2004. Google Scholar
  7. 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
  8. 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
  9. C. 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
  10. 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
  11. G. L. Burn, C. Hankin, and S. Abramsky. Strictness analysis for higher-order functions. Sci. Comp. Prog., 7(3):249-278, 1986. Google Scholar
  12. T. Cachat. Symbolic strategy synthesis for games on pushdown graphs. In ICALP, volume 2380 of LNCS, pages 704-715. Springer, 2002. Google Scholar
  13. T. Cachat. Higher order pushdown automata, the Caucal hierarchy of graphs and parity games. In ICALP, volume 2719 of LNCS, pages 556-569. Springer, 2003. Google Scholar
  14. D. Caucal. On infinite terms having a decidable monadic theory. In MFCS, volume 2420 of LNCS, pages 165-176. Springer, 2002. Google Scholar
  15. P. Cousot and R. Cousot. Higher order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection, and PER analysis. In ICCL, pages 95-112. IEEE, 1994. Google Scholar
  16. W. Damm. The IO- and OI-hierarchies. Theor. Comp. Sci., 20:95-207, 1982. Google Scholar
  17. W. Damm and A. Goerdt. An automata-theoretical characterization of the OI-hierarchy. Inf. Comp., 71:1-32, 1986. Google Scholar
  18. A. Farzan, Z. Kincaid, and A. Podelski. Proof spaces for unbounded parallelism. In POPL, pages 407-420. ACM, 2015. Google Scholar
  19. A. Farzan, Z. Kincaid, and A. Podelski. Proving liveness of parameterized programs. In LICS, pages 185-196. IEEE, 2016. Google Scholar
  20. Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Proofs that count. In POPL, pages 151-164. ACM, 2014. Google Scholar
  21. A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. ENTCS, 9:27-37, 1997. Google Scholar
  22. S. Fogarty and M. Y. Vardi. Efficient Büchi universality checking. In TACAS, volume 6015 of LNCS, pages 205-220. Springer, 2010. Google Scholar
  23. C. Grellois. Semantics of linear logic and higher-order model-checking. PhD thesis, Université Paris Diderot (Paris 7), 2016. Google Scholar
  24. 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
  25. C. Grellois and P.-A. Melliès. An infinitary model of linear logic. In FoSSaCS, volume 9034 of LNCS, pages 41-55. Springer, 2015. Google Scholar
  26. C. Grellois and P.-A. Melliès. Relational semantics of linear logic and higher-order model checking. In CSL, volume 41 of LIPIcs, pages 260-276. Dagstuhl, 2015. Google Scholar
  27. A. Haddad. IO vs OI in higher-order recursion schemes. In FICS, volume 77 of EPTCS, pages 23-30, 2012. Google Scholar
  28. M. Hague, R. Meyer, and S. Muskalla. Domains for higher-order games. CoRR, abs/1705.00355, 2017. URL: http://arxiv.org/abs/1705.00355.
  29. M. Hague, A. S. Murawski, C.-H. L. Ong, and O. Serre. Collapsible pushdown automata and recursion schemes. In LICS, pages 452-461. IEEE, 2008. Google Scholar
  30. M. Hague and C.-H. L. Ong. Symbolic backwards-reachability analysis for higher-order pushdown systems. In FoSSaCS, volume 4423 of LNCS, pages 213-227. Springer, 2007. Google Scholar
  31. 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
  32. M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL, pages 471-482. ACM, 2010. Google Scholar
  33. M. Hofmann and W. Chen. Abstract interpretation from Büchi automata. In CSL-LICS, pages 51:1-51:10, 2014. Google Scholar
  34. M. Hofmann and J. Ledent. A cartesian-closed category for higher-order model checking. In LICS. IEEE, 2017. To appear. Google Scholar
  35. L. Holík, R. Meyer, and S. Muskalla. Summaries for context-free games. In FSTTCS, volume 65 of LIPIcs, pages 41:1-41:16. Dagstuhl, 2016. Google Scholar
  36. Lukás Holík and Roland Meyer. Antichains for the verification of recursive programs. In NETYS, volume 9466 of LNCS, pages 322-336. Springer, 2015. Google Scholar
  37. T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS, volume 2303 of LNCS, pages 205-222. Springer, 2002. Google Scholar
  38. T. Knapik, D. Niwiński, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. In ICALP, volume 3580 of LNCS, pages 1450-1461. Springer, 2005. Google Scholar
  39. N. Kobayashi. HorSat2: A model checker for HORS based on SATuration. A tool available at URL: http://www-kb.is.s.u-tokyo.ac.jp/~koba/horsat2/.
  40. N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, pages 416-428. ACM, 2009. Google Scholar
  41. 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
  42. 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
  43. D. A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. URL: http://www.jstor.org/stable/1971035.
  44. R. Meyer, S. Muskalla, and E. Neumann. Liveness verification and synthesis: New algorithms for recursive programs. URL: https://arxiv.org/abs/1701.02947.
  45. C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81-90. IEEE, 2006. Google Scholar
  46. S. J. Ramsay. Intersection-Types and Higher-Order Model Checking. PhD thesis, Oxford University, 2013. Google Scholar
  47. S. J. Ramsay. Exact intersection type abstractions for safety checking of recursion schemes. In PPDP, pages 175-186. ACM, 2014. Google Scholar
  48. S. Salvati. Recognizability in the simply typed lambda-calculus. In WoLLIC, volume 5514 of LNCS, pages 48-60. Springer, 2009. Google Scholar
  49. 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
  50. S. Salvati and I. Walukiewicz. Typing weak MSOL properties. In FoSSaCS, volume 9034 of LNCS, pages 343-357. Springer, 2015. Google Scholar
  51. S. Salvati and I. Walukiewicz. Using models to model-check recursive schemes. LMCS, 11(2):1-23, 2015. Google Scholar
  52. I. Walukiewicz. Pushdown processes: Games and model-checking. Inf. Comp., 164(2):234-263, 2001. Google Scholar
  53. 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, pages 17-30. 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 Imprint Privacy Contact