88 citations · 339 across the 67 of their papers we have counts for
30 papers · 1 filter
Compositional Verification of Almost-Sure Büchi Objectives in MDPs
Marck van der Vegt, Kazuki Watanabe, Ichiro Hasuo +1
This paper studies the verification of almost-sure Büchi objectives in MDPs with a known, compositional structure based on string diagrams. In particular, we ask whether there is a…
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…
Compositional Value Iteration with Pareto Caching
Kazuki Watanabe, Marck van der Vegt, Sebastian Junges +1
The de-facto standard approach in MDP verification is based on value iteration (VI). We propose compositional VI, a framework for model checking compositional MDPs, that addresses…
Pareto Curves for Compositionally Model Checking String Diagrams of MDPs
Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo +2
Computing schedulers that optimize reachability probabilities in MDPs is a standard verification task. To address scalability concerns, we focus on MDPs that are compositionally de…
Compositional Probabilistic Model Checking with String Diagrams of MDPs
Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada +1
We present a compositional model checking algorithm for Markov decision processes, in which they are composed in the categorical graphical language of string diagrams. The algorith…
Compositional Solution of Mean Payoff Games by String Diagrams
Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada +1
Following our recent development of a compositional model checking algorithm for Markov decision processes, we present a compositional framework for solving mean payoff games (MPGs…
Exploiting Adjoints in Property Directed Reachability Analysis
Mayuko Kori, Flavio Ascari, Filippo Bonchi +3
We formulate, in lattice-theoretic terms, two novel algorithms inspired by Bradley's property directed reachability algorithm. For finding safe invariants or counterexamples, the f…
The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata +2
We present LT-PDR, a lattice-theoretic generalization of Bradley's property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious…
Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation
Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke +2
A modal logic that is strong enough to fully characterize the behavior of a system is called expressive. Recently, with the growing diversity of systems to be reasoned about (proba…
Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down
Mayuko Kori, Ichiro Hasuo, Shin-ya Katsumata
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, w…
Decision Tree Learning in CEGIS-Based Termination Analysis
Satoshi Kura, Hiroshi Unno, Ichiro Hasuo
We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample G…
Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
Kittiphon Phalakarn, Toru Takisaka, Thomas Haas +1
Solving stochastic games with the reachability objective is a fundamental problem, especially in quantitative verification and synthesis. For this purpose, bounded value iteration…
Codensity Games for Bisimilarity
Yuichi Komorida, Shin-ya Katsumata, Nick Hu +2
Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, et…
Relational Differential Dynamic Logic
Juraj Kolčák, Ichiro Hasuo, Jérémy Dubut +3
In the field of quality assurance of hybrid systems (that combine continuous physical dynamics and discrete digital control), Platzer's differential dynamic logic (dL) is widely re…
Quantitative Simulations by Matrices
Natsuki Urabe, Ichiro Hasuo
We introduce notions of simulation between semiring-weighted automata as models of quantitative systems. Our simulations are instances of the categorical/coalgebraic notions previo…
Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
Satoshi Kura, Natsuki Urabe, Ichiro Hasuo
Programs with randomization constructs is an active research topic, especially after the recent introduction of martingale-based analysis methods for their termination and runtimes…
Quantitative bisimulations using coreflections and open morphisms
Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata +1
We investigate a canonical way of defining bisimilarity of systems when their semantics is given by a coreflection, typically in a category of transition systems. We use the fact,…
Categorical Buechi and Parity Conditions via Alternating Fixed Points of Functors
Natsuki Urabe, Ichiro Hasuo
Categorical studies of recursive data structures and their associated reasoning principles have mostly focused on two extremes: initial algebras and induction, and final coalgebras…
Sharper and Simpler Nonlinear Interpolants for Program Verification
Takamasa Okudono, Yuki Nishida, Kensuke Kojima +3
Interpolation of jointly infeasible predicates plays important roles in various program verification techniques such as invariant synthesis and CEGAR. Intrigued by the recent resul…
Categorical Liveness Checking by Corecursive Algebras
Natsuki Urabe, Masaki Hara, Ichiro Hasuo
Final coalgebras as "categorical greatest fixed points" play a central role in the theory of coalgebras. Somewhat analogously, most proof methods studied therein have focused on gr…
Coalgebraic Trace Semantics for Buechi and Parity Automata
Natsuki Urabe, Shunsuke Shimizu, Ichiro Hasuo
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 no…
Fair Simulation for Nondeterministic and Probabilistic Buechi Automata: a Coalgebraic Perspective
Natsuki Urabe, Ichiro Hasuo
Notions of simulation, among other uses, provide a computationally tractable and sound (but not necessarily complete) proof method for language inclusion. They have been comprehens…
Semantics of Higher-Order Quantum Computation via Geometry of Interaction
Ichiro Hasuo, Naohiko Hoshino
While much of the current study on quantum computation employs low-level formalisms such as quantum circuits, several high-level languages/calculi have been recently proposed aimin…
Healthiness from Duality
Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo +1
Healthiness is a good old question in program logics that dates back to Dijkstra. It asks for an intrinsic characterization of those predicate transformers which arise as the (back…