6 papers
From Coalgebraic Determinization to Belief Construction for Partial Observability
Mayuko Kori, Kazuki Watanabe
The belief construction is a fundamental technique for transforming partially observable systems to fully observable ones while preserving the relevant semantics. It plays a centra…
Coalgebraic Non-Wellfounded Proofs: Recursiveness and GTC
Mayuko Kori
Non-wellfounded proof systems impose a global condition called the global trace condition (GTC) on a derivation tree to ensure soundness. Providing a categorical characterisation o…
A Framework for Coalgebraic Reward-Sensitive Bisimulation (Extended Version)
Pedro H. Azevedo de Amorim, Mayuko Kori, Koko Muroya
In this paper we present a framework for modelling \emph{reward-sensitive bisimulations}, that is, bisimulations that account for quantitative differences such as accumulated rewar…
A No-go Theorem for Coalgebraic Product Construction
Mayuko Kori, Kazuki Watanabe
Verifying traces of systems is a central topic in formal verification. We study model checking of Markov chains (MCs) against temporal properties represented as (finite) automata.…
A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs
Kazuki Watanabe, Mayuko Kori, Taro Sekiyama +2
We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a…
Initial Algebra Correspondence under Reachability Conditions
Mayuko Kori, Kazuki Watanabe, Jurriaan Rot
Suitable reachability conditions can make two different fixed point semantics of a transition system coincide. For instance, the total and partial expected reward semantics on Mark…