Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

On Higher-Order Reachability Games Vs May Reachability

  • Conference paper
  • First Online:
Reachability Problems (RP 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13608))

Included in the following conference series:

Abstract

We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with angelic and demonic nondeterminism) and may-reachability (i.e., the reachability problem for programs with only angelic nondeterminism). We show that reachability games for order-\(n\) programs can be reduced to may-reachability problems for order-(\(n+1\)) programs, and vice versa. We formalize the reductions by using higher-order fixpoint logic and prove their correctness. We also discuss applications to higher-order program verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 59.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    In the context of program verification, we are often interested in (un)reachability to bad states. Thus, in that context, \(\textbf{succ}\) in this section is actually interpreted as an error state, and the terms “angelic” and “demonic” below are swapped.

  2. 2.

    Although the understanding of the refinement type systems ReTHFL is not required below, interested readers may wish to consult [11].

  3. 3.

    We have implemented a prototype translator, but have not yet integrated it into ReTHFL. For readability, here we show the formula obtained by some manual simplification of the automatically generated formula.

References

  1. Asada, K., Katsura, H., Kobayashi, N.: On higher-order reachability games vs may reachability. CoRR abs/2203.08416 (2022). https://doi.org/10.48550/arXiv.2203.08416

  2. Asada, K., Kobayashi, N.: On word and frontier languages of unsafe higher-order grammars. In: Chatzigiannakis, I., Mitzenmacher, M., Rabani, Y., Sangiorgi, D. (eds.) 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, 11–15 July 2016, Rome, Italy. LIPIcs, vol. 55, pp. 111:1–111:13. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016). https://doi.org/10.4230/LIPIcs.ICALP.2016.111

  3. Asada, K., Kobayashi, N.: Size-preserving translations from order-(n+1) word grammars to order-n tree grammars. In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29–July 6 2020, Paris, France (Virtual Conference). LIPIcs, vol. 167, pp. 22:1–22:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/LIPIcs.FSCD.2020.22

  4. Burn, T.C., Ong, C.L., Ramsay, S.J.: Higher-order constrained Horn clauses for verification. Proc. ACM Program. Lang. 2(POPL), 11:1–11:28 (2018). https://doi.org/10.1145/3158099

  5. Champion, A., Chiba, T., Kobayashi, N., Sato, R.: ICE-based refinement type discovery for higher-order functional programs. J. Autom. Reason. 64(7), 1393–1418 (2020). https://doi.org/10.1007/s10817-020-09571-y

  6. Champion, A., Kobayashi, N., Sato, R.: HoIce: An ICE-based non-linear horn clause solver. In: Ryu, S. (ed.) Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2–6, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11275, pp. 146–156. Springer (2018). https://doi.org/10.1007/978-3-030-02768-1_8

  7. Damm, W.: The IO- and OI-hierarchies. Theor. Comput. Sci. 20, 95–207 (1982)

    Article  MathSciNet  Google Scholar 

  8. Grädel, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games: A Guide to Current Research, LNCS, vol. 2500. Springer, Cham (2002). https://doi.org/10.1007/3-540-36387-4

    Book  MATH  Google Scholar 

  9. Hojjat, H., Rümmer, P.: The ELDARICA horn solver. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1–7 (2018)

    Google Scholar 

  10. Iwayama, N., Kobayashi, N., Suzuki, R., Tsukada, T.: Predicate abstraction and CEGAR for \(\nu \)HFL\(_Z\) validity checking. In: Pichardie, D., Sighireanu, M. (eds.) SAS 2020. LNCS, vol. 12389, pp. 134–155. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-65474-0_7

    Chapter  Google Scholar 

  11. Katsura, H., Iwayama, N., Kobayashi, N., Tsukada, T.: A new refinement type system for automated \(\nu \)HFL\(_Z\) validity checking. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 86–104. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-64437-6_5

    Chapter  Google Scholar 

  12. Kobayashi, N., Dal Lago, U., Grellois, C.: On the termination problem for probabilistic higher-order recursive programs. In: Proceedings of LICS 2019. IEEE (2019)

    Google Scholar 

  13. Kobayashi, N., Nishikawa, T., Igarashi, A., Unno, H.: Temporal verification of programs via first-order fixpoint logic. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 413–436. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32304-2_20

    Chapter  Google Scholar 

  14. Kobayashi, N., Ong, C.-H.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 223–234. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02930-1_19

    Chapter  Google Scholar 

  15. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI 2011, pp. 222–233. ACM Press (2011)

    Google Scholar 

  16. Kobayashi, N., Tsukada, T., Watanabe, K.: Higher-order program verification via HFL model checking. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 711–738. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_25

    Chapter  Google Scholar 

  17. Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175–205 (2016). https://doi.org/10.1007/s10703-016-0249-4

    Article  MATH  Google Scholar 

  18. Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS 2006, pp. 81–90. IEEE Computer Society Press (2006)

    Google Scholar 

  19. Parys, P.: Higher-order model checking step by step. In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12–16, 2021, Glasgow, Scotland (Virtual Conference). LIPIcs, vol. 198, pp. 140:1–140:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.ICALP.2021.140

  20. Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI 2008, pp. 159–169 (2008)

    Google Scholar 

  21. Satake, Y., Unno, H., Yanagi, H.: Probabilistic inference for predicate constraint satisfaction. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, pp. 1644–1651. AAAI Press (2020)

    Google Scholar 

  22. Tsukada, T.: On computability of logical approaches to branching-time property verification of programs. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) LICS 2020: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, 8–11 July 2020, pp. 886–899. ACM (2020). https://doi.org/10.1145/3373718.3394766

  23. Viswanathan, M., Viswanathan, R.: A higher order modal fixed point logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 512–528. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_33

    Chapter  Google Scholar 

  24. Watanabe, K., Tsukada, T., Oshikawa, H., Kobayashi, N.: Reduction from branching-time property verification of higher-order programs to HFL validity checking. In: Hermenegildo, M.V., Igarashi, A. (eds.) Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, 14–15 January 2019, pp. 22–34. ACM (2019). https://doi.org/10.1145/3294032.3294077

Download references

Acknowledgments

We would like to thank anonymous referees for useful comments. This work was supported by JSPS KAKENHI Grant Number JP20H05703 and JST SPRING Grant Number JPMJSP2108.

Author information

Authors and Affiliations

  1. Tohoku University, Sendai, Japan

    Kazuyuki Asada

  2. The University of Tokyo, Tokyo, Japan

    Hiroyuki Katsura & Naoki Kobayashi

Authors
  1. Kazuyuki Asada
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hiroyuki Katsura
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Naoki Kobayashi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Naoki Kobayashi .

Editor information

Editors and Affiliations

  1. Department of Computer Science, TU Kaiserslautern, Kaiserslautern, Germany

    Anthony W. Lin

  2. Max Planck Institute for Software Systems, Kaiserslautern, Germany

    Georg Zetzsche

  3. University of Liverpool, Liverpool, UK

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Asada, K., Katsura, H., Kobayashi, N. (2022). On Higher-Order Reachability Games Vs May Reachability. In: Lin, A.W., Zetzsche, G., Potapov, I. (eds) Reachability Problems. RP 2022. Lecture Notes in Computer Science, vol 13608. Springer, Cham. https://doi.org/10.1007/978-3-031-19135-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-19135-0_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-19134-3

  • Online ISBN: 978-3-031-19135-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation