59 citations · 152 across the 53 of their papers we have counts for
44 papers · 1 filter
Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis
Christina Gehnen, Dominique Unruh, Joost-Pieter Katoen
Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest…
Compositional Reasoning for Probabilistic Automata with Uncertainty
Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen
This paper develops an assume-guarantee (AG) framework for the compositional verification of probabilistic automata (PAs) with uncertain transition probabilities. We study parametr…
Verification of Robust Multi-Agent Systems
Raphaël Berthon, Joost-Pieter Katoen, Munyque Mittelmann +1
Stochastic multi-agent systems are a central modeling framework for autonomous controllers, communication protocols, and cyber-physical infrastructures. In many such systems, howev…
Verifying Sampling Algorithms via Distributional Invariants
Daniel Zilken, Kevin Batz, Joost-Pieter Katoen +1
This paper presents a Hoare-like veri cation framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso's Fast Dice Roller and Saa…
Compositional Reasoning for Parametric Probabilistic Automata
Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen
We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) - an extension to probabilistic…
Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Timm Spork, Christel Baier, Joost-Pieter Katoen +2
We introduce -bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $(\varepsilo…