TY - GEN
T1 - On average-case hardness of higher-order model checking
AU - Nakamura, Yoshiki
AU - Asada, Kazuyuki
AU - Kobayashi, Naoki
AU - Sin'Ya, Ryoma
AU - Tsukada, Takeshi
N1 - Funding Information:
This work was supported by JSPS Kakenhi 15H05706 and JSPS Kakenhi 20H00577.
Publisher Copyright:
© Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada; licensed under Creative Commons License CC-BY 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020).
PY - 2020/6/1
Y1 - 2020/6/1
N2 - 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.
AB - 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.
KW - Average-case complexity
KW - Higher-order model checking
KW - Intersection type system
UR - http://www.scopus.com/inward/record.url?scp=85089364739&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85089364739&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSCD.2020.21
DO - 10.4230/LIPIcs.FSCD.2020.21
M3 - Conference contribution
AN - SCOPUS:85089364739
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020
A2 - Ariola, Zena M.
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020
Y2 - 29 June 2020 through 6 July 2020
ER -