文章基本信息

标题：On Average-Case Hardness of Higher-Order Model Checking
本地全文：下载
作者：Yoshiki Nakamura ; Kazuyuki Asada ; Naoki Kobayashi 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：167
页码：21:1-21:23
DOI：10.4230/LIPIcs.FSCD.2020.21
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Higher-order model checking; average-case complexity; intersection type system