3 Search Results for "Shimizu, Shunsuke"

Document
DOI: 10.4230/LIPIcs.CSL.2025.28
Strong Induction Is an Up-To Technique

Authors: Filippo Bonchi, Elena Di Lavore, and Anna Ricci

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Up-to techniques are enhancements of the coinduction proof principle which, in lattice theoretic terms, is the dual of induction. What is the dual of coinduction up-to? By means of duality, we illustrate a theory of induction up-to and we observe that an elementary proof technique, commonly known as strong induction, is an instance of induction up-to. We also show that, when generalising our theory from lattices to categories, one obtains an enhancement of the induction definition principle known in the literature as comonadic recursion.
Cite as

Filippo Bonchi, Elena Di Lavore, and Anna Ricci. Strong Induction Is an Up-To Technique. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CSL.2025.28,
  author =	{Bonchi, Filippo and Di Lavore, Elena and Ricci, Anna},
  title =	{{Strong Induction Is an Up-To Technique}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.28},
  URN =		{urn:nbn:de:0030-drops-227856},
  doi =		{10.4230/LIPIcs.CSL.2025.28},
  annote =	{Keywords: Induction, Coinduction, Up-to Techniques, Induction up-to, Lattices, Algebras}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.7
Parity Automata for Quantitative Linear Time Logics

Authors: Corina Cirstea, Shunsuke Shimizu, and Ichiro Hasuo

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
We initiate a study of automata-based model checking for previously proposed quantitative linear time logics interpreted over coalgebras. Our results include: (i) an automata-theoretic characterisation of the semantics of these logics, based on a notion of extent of a quantitative parity automaton, (ii) a study of the expressive power of Buchi variants of such automata, with implications on the expressiveness of fragments of the logics considered, and (iii) a naive algorithm for computing extents, under additional assumptions on the domain of truth values.
Cite as

Corina Cirstea, Shunsuke Shimizu, and Ichiro Hasuo. Parity Automata for Quantitative Linear Time Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cirstea_et_al:LIPIcs.CALCO.2017.7,
  author =	{Cirstea, Corina and Shimizu, Shunsuke and Hasuo, Ichiro},
  title =	{{Parity Automata for Quantitative Linear Time Logics}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.7},
  URN =		{urn:nbn:de:0030-drops-80468},
  doi =		{10.4230/LIPIcs.CALCO.2017.7},
  annote =	{Keywords: coalgebra, quantitative logic, linear time logic, parity automaton}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.24
Coalgebraic Trace Semantics for Buechi and Parity Automata

Authors: Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Despite its success in producing numerous general results on state-based dynamics, the theory of coalgebra has struggled to accommodate the Buechi acceptance condition---a basic notion in the theory of automata for infinite words or trees. In this paper we present a clean answer to the question that builds on the "maximality" characterization of infinite traces (by Jacobs and Cirstea): the accepted language of a Buechi automaton is characterized by two commuting diagrams, one for a least homomorphism and the other for a greatest, much like in a system of (least and greatest) fixed-point equations. This characterization works uniformly for the nondeterministic branching and the probabilistic one; and for words and trees alike. We present our results in terms of the parity acceptance condition that generalizes Buechi's.
Cite as

Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic Trace Semantics for Buechi and Parity Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{urabe_et_al:LIPIcs.CONCUR.2016.24,
  author =	{Urabe, Natsuki and Shimizu, Shunsuke and Hasuo, Ichiro},
  title =	{{Coalgebraic Trace Semantics for Buechi and Parity Automata}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.24},
  URN =		{urn:nbn:de:0030-drops-61867},
  doi =		{10.4230/LIPIcs.CONCUR.2016.24},
  annote =	{Keywords: coalgebra, Buechi automaton, parity automaton, probabilistic automaton, tree automaton}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2017
  • 1 2016

  • Refine by Author
  • 2 Hasuo, Ichiro
  • 2 Shimizu, Shunsuke
  • 1 Bonchi, Filippo
  • 1 Cirstea, Corina
  • 1 Di Lavore, Elena
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 2 coalgebra
  • 2 parity automaton
  • 1 Algebras
  • 1 Buechi automaton
  • 1 Coinduction
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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