1 Search Results for "Sin'ya, Ryoma"

Document
DOI: 10.4230/LIPIcs.FSCD.2020.21
On Average-Case Hardness of Higher-Order Model Checking

Authors: Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

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.
Cite as

Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, and Takeshi Tsukada. On Average-Case Hardness of Higher-Order Model Checking. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{nakamura_et_al:LIPIcs.FSCD.2020.21,
  author =	{Nakamura, Yoshiki and Asada, Kazuyuki and Kobayashi, Naoki and Sin'ya, Ryoma and Tsukada, Takeshi},
  title =	{{On Average-Case Hardness of Higher-Order Model Checking}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{21:1--21:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.21},
  URN =		{urn:nbn:de:0030-drops-123439},
  doi =		{10.4230/LIPIcs.FSCD.2020.21},
  annote =	{Keywords: Higher-order model checking, average-case complexity, intersection type system}
}
  • Refine by Author
  • 1 Asada, Kazuyuki
  • 1 Kobayashi, Naoki
  • 1 Nakamura, Yoshiki
  • 1 Sin'ya, Ryoma
  • 1 Tsukada, Takeshi

  • Refine by Classification
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 1 Higher-order model checking
  • 1 average-case complexity
  • 1 intersection type system

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2020

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact