2026-08-07T09:32:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12343 2024-03-06T10:50:00Z ddc:004 open_access

On Average-Case Hardness of Higher-Order Model Checking Nakamura, Yoshiki Asada, Kazuyuki Kobayashi, Naoki Sin'ya, Ryoma Tsukada, Takeshi Higher-order model checking average-case complexity intersection type system 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yoshiki Nakamura and Kazuyuki Asada and Naoki Kobayashi and Ryoma Sin'ya and Takeshi Tsukada 2020 Is Part Of LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2020.21 urn:nbn:de:0030-drops-123439 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.21 eng https://creativecommons.org/licenses/by/3.0/legalcode