Search Results

Documents authored by Tsukada, Takeshi

Document
DOI: 10.4230/LIPIcs.FSCD.2021.32
Output Without Delay: A π-Calculus Compatible with Categorical Semantics

Authors: Ken Sakayori and Takeshi Tsukada

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
The quest for logical or categorical foundations of the π-calculus (not limited to session-typed variants) remains an important challenge. A categorical type theory correspondence for a variant of the i/o-typed π-calculus was recently revealed by Sakayori and Tsukada, but, at the same time, they exposed that this categorical semantics contradicts with most of the behavioural equivalences. This paper diagnoses the nature of this problem and attempts to fill the gap between categorical and operational semantics. We first identify the source of the problem to be the mismatch between the operational and categorical interpretation of a process called the forwarder. From the operational viewpoint, a forwarder may add an arbitrary delay when forwarding a message, whereas, from the categorical viewpoint, a forwarder must not add any delay when forwarding a message. Led by this observation, we introduce a calculus that can express forwarders that do not introduce delay. More specifically, the calculus we introduce is a variant of the π-calculus with a new operational semantics in which output actions are forced to happen as soon as they get unguarded. We show that this calculus (i) is compatible with the categorical semantics and (ii) can encode the standard π-calculus.
Cite as

Ken Sakayori and Takeshi Tsukada. Output Without Delay: A π-Calculus Compatible with Categorical Semantics. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 32:1-32:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{sakayori_et_al:LIPIcs.FSCD.2021.32,
  author =	{Sakayori, Ken and Tsukada, Takeshi},
  title =	{{Output Without Delay: A \pi-Calculus Compatible with Categorical Semantics}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{32:1--32:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.32},
  URN =		{urn:nbn:de:0030-drops-142705},
  doi =		{10.4230/LIPIcs.FSCD.2021.32},
  annote =	{Keywords: \pi-calculus, categorical semantics, linear approximation}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.29
A Cyclic Proof System for HFL_ℕ

Authors: Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
A cyclic proof system allows us to perform inductive reasoning without explicit inductions. We propose a cyclic proof system for HFL_ℕ, which is a higher-order predicate logic with natural numbers and alternating fixed-points. Ours is the first cyclic proof system for a higher-order logic, to our knowledge. Due to the presence of higher-order predicates and alternating fixed-points, our cyclic proof system requires a more delicate global condition on cyclic proofs than the original system of Brotherston and Simpson. We prove the decidability of checking the global condition and soundness of this system, and also prove a restricted form of standard completeness for an infinitary variant of our cyclic proof system. A potential application of our cyclic proof system is semi-automated verification of higher-order programs, based on Kobayashi et al.’s recent work on reductions from program verification to HFL_ℕ validity checking.
Cite as

Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi. A Cyclic Proof System for HFL_ℕ. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kori_et_al:LIPIcs.CSL.2021.29,
  author =	{Kori, Mayuko and Tsukada, Takeshi and Kobayashi, Naoki},
  title =	{{A Cyclic Proof System for HFL\underline\mathbb{N}}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{29:1--29:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.29},
  URN =		{urn:nbn:de:0030-drops-134632},
  doi =		{10.4230/LIPIcs.CSL.2021.29},
  annote =	{Keywords: Cyclic proof, higher-order logic, fixed-point logic, sequent calculus}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.19
A Probabilistic Higher-Order Fixpoint Logic

Authors: Yo Mitani, Naoki Kobayashi, and Takeshi Tsukada

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

Abstract
We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the μ^p-calculus. We show that PHFL is strictly more expressive than the μ^p-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the μ-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky’s μ-arithmetic to PHFL, which implies that PHFL model checking is Π^1₁-hard and Σ^1₁-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.
Cite as

Yo Mitani, Naoki Kobayashi, and Takeshi Tsukada. A Probabilistic Higher-Order Fixpoint Logic. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{mitani_et_al:LIPIcs.FSCD.2020.19,
  author =	{Mitani, Yo and Kobayashi, Naoki and Tsukada, Takeshi},
  title =	{{A Probabilistic Higher-Order Fixpoint Logic}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{19:1--19:22},
  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.19},
  URN =		{urn:nbn:de:0030-drops-123413},
  doi =		{10.4230/LIPIcs.FSCD.2020.19},
  annote =	{Keywords: Probabilistic logics, higher-order fixpoint logic, model checking}
}
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}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2017.32
Streett Automata Model Checking of Higher-Order Recursion Schemes

Authors: Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, and Takeshi Tsukada

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

Abstract
We propose a practical algorithm for Streett automata model checking of higher-order recursion schemes (HORS), which checks whether the tree generated by a given HORS is accepted by a given Streett automaton. The Streett automata model checking of HORS is useful in the context of liveness verification of higher-order functional programs. The previous approach to Streett automata model checking converted Streett automata to parity automata and then invoked a parity tree automata model checker. We show through experiments that our direct approach outperforms the previous approach. Besides being able to directly deal with Streett automata, our algorithm is the first practical Streett or parity automata model checking algorithm that runs in time polynomial in the size of HORS, assuming that the other parameters are fixed. Previous practical fixed-parameter polynomial time algorithms for HORS could only deal with the class of trivial tree automata. We have confirmed through experiments that (a parity automata version of) our model checker outperforms previous parity automata model checkers for HORS.
Cite as

Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, and Takeshi Tsukada. Streett Automata Model Checking of Higher-Order Recursion Schemes. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{suzuki_et_al:LIPIcs.FSCD.2017.32,
  author =	{Suzuki, Ryota and Fujima, Koichi and Kobayashi, Naoki and Tsukada, Takeshi},
  title =	{{Streett Automata Model Checking of Higher-Order Recursion Schemes}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{32:1--32:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.32},
  URN =		{urn:nbn:de:0030-drops-77325},
  doi =		{10.4230/LIPIcs.FSCD.2017.32},
  annote =	{Keywords: Higher-order model checking, higher-order recursion schemes, Streett automata}
}
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