On average-case hardness of higher-order model checking

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publication5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020
EditorsZena M. Ariola
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959771559
DOIs
Publication statusPublished - 2020 Jun 1
Event5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020 - Virtual, Online, France
Duration: 2020 Jun 292020 Jul 6

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume167
ISSN (Print)1868-8969

Conference

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

Keywords

  • Average-case complexity
  • Higher-order model checking
  • Intersection type system

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'On average-case hardness of higher-order model checking'. Together they form a unique fingerprint.

Cite this