The papers “Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains” by Timm Spork, Christel Baier, Joost-Pieter Katoen, Sascha Klüppelholz, and Jakob Piribauer and “Efficient Probabilistic Model Checking for Relational Reachability” by Lina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpour and Sebastian Junges have been accepted at the International Conference on Computer-Aided Verification (CAV) 2025.

The first paper presents a new notion of approximate bisimulation on CTMCs that allows for perturbations of exit rates as well as transition probabilities. The paper investigates several properties, in particular it provides bounds for preserving time-bounded reachanility probabilities in CTMCs.

The second paper introduces relational reachability properties on MDPs (e.g., reaching two different targets with equal probability) and provides an efficient model checking algorithm.