Document Open Access Logo

On Average-Case Hardness of Higher-Order Model Checking

Authors Yoshiki Nakamura , Kazuyuki Asada , Naoki Kobayashi , Ryoma Sin'ya , Takeshi Tsukada

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.21.pdf
  • Filesize: 1.11 MB
  • 23 pages

Document Identifiers

Author Details

Yoshiki Nakamura
  • Tokyo Institute of Technology, Japan
Kazuyuki Asada
  • Tohoku University, Sendai, Japan
Naoki Kobayashi
  • The University of Tokyo, Japan
Ryoma Sin'ya
  • Akita University, Japan
Takeshi Tsukada
  • The University of Tokyo, Japan

Funding

This work was supported by JSPS Kakenhi 15H05706 and JSPS Kakenhi 20H00577.

Acknowledgements

We would like to thank anonymous referees for useful comments.

Cite AsGet BibTex

Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada. On Average-Case Hardness of Higher-Order Model Checking. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.21

Abstract

We study a mixture between the average case and worst case complexities of higher-order model checking, the problem of deciding whether the tree generated by a given λ Y-term (or equivalently, a higher-order recursion scheme) satisfies the property expressed by a given tree automaton. Higher-order model checking has recently been studied extensively in the context of higher-order program verification. Although the worst-case complexity of the problem is k-EXPTIME complete for order-k terms, various higher-order model checkers have been developed that run efficiently for typical inputs, and program verification tools have been constructed on top of them. One may, therefore, hope that higher-order model checking can be solved efficiently in the average case, despite the worst-case complexity. We provide a negative result, by showing that, under certain assumptions, for almost every term, the higher-order model checking problem specialized for the term is k-EXPTIME hard with respect to the size of automata. The proof is based on a novel intersection type system that characterizes terms that do not contain any useless subterms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • Higher-order model checking
  • average-case complexity
  • intersection type system

Metrics

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

Related Versions

References

  1. Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada. Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. Logical Methods in Computer Science, 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:16)2019.
  2. Maciej Bendkowski, Katarzyna Grygiel, and Marek Zaionc. On the likelihood of normalization in combinatory logic. J. Log. Comput., 27(7):2251-2269, 2017. URL: https://doi.org/10.1093/logcom/exx005.
  3. Andrej Bogdanov and Luca Trevisan. Average-case complexity. CoRR, abs/cs/0606037, 2006. URL: http://arxiv.org/abs/cs/0606037.
  4. Christopher H. Broadbent and Naoki Kobayashi. Saturation-based model checking of higher-order recursion schemes. In Proceedings of Computer Science Logic (CSL), volume 23 of LIPIcs, pages 129-148. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.129.
  5. Pierre Clairambault, Charles Grellois, and Andrzej S. Murawski. Linearity in higher-order recursion schemes. PACMPL, 2(POPL):39:1-39:29, 2018. URL: https://doi.org/10.1145/3158127.
  6. Mario Coppo, Ferruccio Damiani, and Paola Giannini. Refinement types for program analysis. In Proceedings of International Static Analysis Symposium (SAS), volume 1145 of Lecture Notes in Computer Science, pages 143-158. Springer, 1996. URL: https://doi.org/10.1007/3-540-61739-6_39.
  7. Ferruccio Damiani. A conjunctive type system for useless-code elimination. Mathematical Structures in Computer Science, 13(1):157-197, 2003. URL: https://doi.org/10.1017/S0960129502003869.
  8. René David, Katarzyna Grygiel, Jakub Kozik, Christophe Raffalli, Guillaume Theyssier, and Marek Zaionc. Asymptotically almost all λ-terms are strongly normalizing. Logical Methods in Computer Science, 9(1), 2013. URL: https://doi.org/10.2168/LMCS-9(1:2)2013.
  9. Philippe Flajolet and Robert Sedgewick. Analytic Combinatorics. Cambridge University Press, 1 edition, 2009. URL: https://doi.org/10.1017/CBO9780511801655.
  10. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. URL: https://doi.org/10.1007/3-540-36387-4.
  11. Ilya Kapovich, Alexei G. Myasnikov, Paul Schupp, and Vladimir Shpilrain. Generic-case complexity, decision problems in group theory and random walks. CoRR, abs/math/0203239, 2002. URL: https://arxiv.org/abs/math/0203239.
  12. Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. Higher-order pushdown trees are easy. In Proceedings of International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 2303 of Lecture Notes in Computer Science, pages 205-222. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_15.
  13. Naoki Kobayashi. Type-based useless-variable elimination. Higher-Order and Symbolic Computation, 14(2-3):221-260, 2001. URL: https://doi.org/10.1023/A:1012944815270.
  14. Naoki Kobayashi. Model-checking higher-order functions. In Proceedings of ACM SIGPLAN conference on Principles and Practice of Declarative Programming (PPDP), pages 25-36. ACM Press, 2009. URL: https://doi.org/10.1145/1599410.1599415.
  15. Naoki Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL), pages 416-428. ACM Press, 2009. URL: https://doi.org/10.1145/1594834.1480933.
  16. Naoki Kobayashi. Model checking higher-order programs. Journal of the ACM, 60(3), 2013. URL: https://doi.org/10.1145/2487241.2487246.
  17. Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of IEEE Symposium on Logic in Computer Science (LICS), pages 179-188. IEEE Computer Society Press, 2009. URL: https://doi.org/10.1109/LICS.2009.29.
  18. Naoki Kobayashi and C.-H. Luke Ong. Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. Logical Methods in Computer Science, 7(4), 2012. URL: https://doi.org/10.2168/LMCS-7(4:9)2011.
  19. Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. Predicate abstraction and CEGAR for higher-order model checking. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 222-233. ACM Press, 2011. URL: https://doi.org/10.1145/1993498.1993525.
  20. Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada. On average-case hardness of higher-order model checking. A full version. Available from URL: https://www.kb.is.s.u-tokyo.ac.jp/~koba/papers/OnAverageCaseHOMC.pdf.
  21. C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In Proceedings of IEEE Symposium on Logic in Computer Science (LICS), pages 81-90. IEEE Computer Society Press, 2006. URL: https://doi.org/10.1109/LICS.2006.38.
  22. C.-H. Luke Ong and Steven Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL), pages 587-598. ACM Press, 2011. URL: https://doi.org/10.1145/1925844.1926453.
  23. Steven Ramsay, Robin Neatherway, and C.-H. Luke Ong. A type-directed abstraction refinement approach to higher-order model checking. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL), pages 61-72. ACM Press, 2014. URL: https://doi.org/10.1145/2535838.2535873.
  24. Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. In Proceedings of International Colloquium on Automata, Languages, and Programming (ICALP), volume 6756 of Lecture Notes in Computer Science, pages 162-173. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22012-8_12.
  25. Sylvain Salvati and Igor Walukiewicz. Recursive schemes, krivine machines, and collapsible pushdown automata. In Proceedings of International Workshop on Reachability Problems (RP), volume 7550 of Lecture Notes in Computer Science, pages 6-20. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33512-9_2.
  26. Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, and Takeshi Tsukada. Almost every simply typed λ-term has a long β-reduction sequence. In Proceedings of International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 10203 of Lecture Notes in Computer Science, pages 53-68. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_4.
  27. Richard Statman. On the lambda Y calculus. APAL, 130(1-3):325-337, 2004. URL: https://doi.org/10.1016/j.apal.2004.04.004.
  28. Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, and Takeshi Tsukada. Streett automata model checking of higher-order recursion schemes. In Proceedings of International Conference on Formal Structures for Computation and Deduction (FSCD), volume 84 of LIPIcs, pages 32:1-32:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.32.
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