Search Results

Documents authored by Nakamura, Yoshiki

Document
DOI: 10.4230/LIPIcs.MFCS.2023.69
On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation

Authors: Yoshiki Nakamura

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
We introduce the k-variable-occurrence fragment, which is the set of terms having at most k occurrences of variables. We give a sufficient condition for the decidability of the equational theory of the k-variable-occurrence fragment using the finiteness of a monoid. As a case study, we prove that for Tarski’s calculus of relations with bounded dot-dagger alternation (an analogy of quantifier alternation in first-order logic), the equational theory of the k-variable-occurrence fragment is decidable for each k.
Cite as

Yoshiki Nakamura. On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 69:1-69:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{nakamura:LIPIcs.MFCS.2023.69,
  author =	{Nakamura, Yoshiki},
  title =	{{On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{69:1--69:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.69},
  URN =		{urn:nbn:de:0030-drops-186030},
  doi =		{10.4230/LIPIcs.MFCS.2023.69},
  annote =	{Keywords: Relation algebra, First-order logic, Decidable fragment, Monoid}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.30
Spatial Existential Positive Logics for Hyperedge Replacement Grammars

Authors: Yoshiki Nakamura

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We study a (first-order) spatial logic based on graphs of conjunctive queries for expressing (hyper-)graph languages. In this logic, each primitive positive (resp. existential positive) formula plays a role of an expression of a graph (resp. a finite language of graphs) modulo graph isomorphism. First, this paper presents a sound- and complete axiomatization for the equational theory of primitive/existential positive formulas under this spatial semantics. Second, we show Kleene theorems between this logic and hyperedge replacement grammars (HRGs), namely that over graphs, the class of existential positive first-order (resp. least fixpoint, transitive closure) formulas has the same expressive power as that of non-recursive (resp. all, linear) HRGs.
Cite as

Yoshiki Nakamura. Spatial Existential Positive Logics for Hyperedge Replacement Grammars. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{nakamura:LIPIcs.CSL.2022.30,
  author =	{Nakamura, Yoshiki},
  title =	{{Spatial Existential Positive Logics for Hyperedge Replacement Grammars}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{30:1--30:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.30},
  URN =		{urn:nbn:de:0030-drops-157504},
  doi =		{10.4230/LIPIcs.CSL.2022.30},
  annote =	{Keywords: Existential positive logic, spatial logic, Kleene theorem}
}
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.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}
}
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 About DROPS Imprint Privacy Contact