On average-case hardness of higher-order model checking

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

研究成果: Conference contribution

抄録

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.

本文言語English
ホスト出版物のタイトル5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020
編集者Zena M. Ariola
出版社Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN(電子版)9783959771559
DOI
出版ステータスPublished - 2020 6 1
イベント5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020 - Virtual, Online, France
継続期間: 2020 6 292020 7 6

出版物シリーズ

名前Leibniz International Proceedings in Informatics, LIPIcs
167
ISSN(印刷版)1868-8969

Conference

Conference5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020
CountryFrance
CityVirtual, Online
Period20/6/2920/7/6

ASJC Scopus subject areas

  • Software

フィンガープリント 「On average-case hardness of higher-order model checking」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル