8 papers
Convex-Analytic View of Query Selection for Safety Verification of Markov Decision Processes
Han Bao, Shinsaku Sakaue, Kazuki Watanabe
Safety verification of a Markov decision process (MDP) asks whether the probabilities of reaching several failure states jointly lie in a convex safe region under every scheduler.…
Specification-Guided Path Shortcutting for Efficient Probabilistic Model Checking
Tsubasa Matsumoto, Kazuki Watanabe, Masaki Waga
Given the safety-critical nature of many embedded systems, their safety assurance is essential. Because such systems are typically stochastic, probabilistic model checking is a par…
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…
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…
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 Unifying Approach to Product Constructions for Quantitative Temporal Inference
Kazuki Watanabe, Sebastian Junges, Jurriaan Rot +1
Probabilistic programs are a powerful and convenient approach to formalise distributions over system executions. A classical verification problem for probabilistic programs is temp…
Composing Codensity Bisimulations
Mayuko Kori, Kazuki Watanabe, Jurriaan Rot +1
Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical for…