Conditional Sampling of Symbolic Markov Chains

Abstract

Probabilistic model checking can compute quantitative properties of stochastic systems by analysing the state space symbolically or numerically. Yet many verification and debugging tasks require concrete executions, and naive random walks (Monte Carlo simulation) become ineffective for rare events because valid traces are exponentially unlikely. Existing rare-event techniques primarily focus on probability estimation and often yield weighted or biased samples, complicating trace-level analysis. In this work, we address conditional sampling: generating execution traces that are exactly distributed according to the model’s dynamics, conditioned on reaching a specific target set. We introduce a symbolic algorithm based on iterative squaring to compute long-distance transition functions, thereby enabling the direct construction of conditional paths without explicit rejection. We implement this approach using two symbolic backends: Algebraic Decision Diagrams (ADDs) and sparse matrices such that the only source of inaccuracy is rounding errors. Our evaluation on the Quantitative Verification Benchmark Set (QVBS) reveals three distinct performance regimes: naive simulation for frequent events, sparse matrices for deep traces in widely connected models, and ADDs for large, structured systems. This capability bridges a gap in formal verification, providing a scalable tool for tasks such as counterexample debugging and estimating path-dependent metrics that rely on inspecting valid behaviours under strict constraints.