Showing 2025Show all
3 papers · 1 filter
cs.LO2025
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…
cs.LO2025
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…
cs.LO2025
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.…