Search Results

Documents authored by Kori, Mayuko

Document
DOI: 10.4230/LIPIcs.CONCUR.2026.39
From Coalgebraic Determinization to Belief Construction for Partial Observability

Authors: Mayuko Kori and Kazuki Watanabe

Published in: LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026)

Abstract
The belief construction is a fundamental technique for transforming partially observable systems to fully observable ones while preserving the relevant semantics. It plays a central role in the analysis of partially observable systems, in particular partially observable Markov decision processes (POMDPs), which is a central model in artificial intelligence and formal verification. In this paper, we develop a coalgebraic framework for the belief construction. To handle observations categorically, we lift a monad to slice categories and introduce a belief decomposition that reorganizes states according to their observations. This allows us to introduce a coalgebraic generalization of the belief construction, obtained by combining the belief decomposition with the coalgebraic determinization of Silva, Bonchi, Bonsangue, and Rutten. In this framework, we show that the semantics of a partially observable system coincides with that of the corresponding belief coalgebra. We then study when the latter further agrees with the semantics of its fully observable counterpart, and use this to identify conditions under which the semantics of a partially observable system coincides with that of the corresponding fully observable belief system. As a consequence, we recover the standard equivalence between POMDPs and belief MDPs, and obtain a new equivalence result for weighted transition systems with the semimodule monad.
Cite as

Mayuko Kori and Kazuki Watanabe. From Coalgebraic Determinization to Belief Construction for Partial Observability. In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 39:1-39:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kori_et_al:LIPIcs.CONCUR.2026.39,
  author =	{Kori, Mayuko and Watanabe, Kazuki},
  title =	{{From Coalgebraic Determinization to Belief Construction for Partial Observability}},
  booktitle =	{37th International Conference on Concurrency Theory (CONCUR 2026)},
  pages =	{39:1--39:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-447-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{391},
  editor =	{Sokolova, Ana and Totzke, Patrick},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.39},
  URN =		{urn:nbn:de:0030-drops-273692},
  doi =		{10.4230/LIPIcs.CONCUR.2026.39},
  annote =	{Keywords: coalgebra, coalgebraic determinization, belief construction, POMDP}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.21
Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

Authors: Mayuko Kori, Ichiro Hasuo, and Shin-ya Katsumata

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of stability of chain colimits; we extend the framework to the presence of a monadic effect, too, restricting to fibrations of complete lattice-valued predicates. Practical benefits of our categorical theory are exemplified by new "upside-down" witness notions for three verification problems: probabilistic liveness, and acceptance and model-checking with respect to bottom-up tree automata.
Cite as

Mayuko Kori, Ichiro Hasuo, and Shin-ya Katsumata. Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kori_et_al:LIPIcs.CONCUR.2021.21,
  author =	{Kori, Mayuko and Hasuo, Ichiro and Katsumata, Shin-ya},
  title =	{{Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{21:1--21:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.21},
  URN =		{urn:nbn:de:0030-drops-143982},
  doi =		{10.4230/LIPIcs.CONCUR.2021.21},
  annote =	{Keywords: initial algebra, final coalgebra, fibration, category theory}
}
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}
}

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