Perturbation resilient equivalences reduce uncertain probabilistic models
Perturbation equivalence in labelled Markov chains
Logic in Computer ScienceFormal Languages and Automata Theory
Summary
When working with models that include chance, small changes in probabilities can cause big differences in how the models behave. The authors study ways to compare parts of these models that stay consistent even if probabilities change, as long as the possible connections remain the same. They define two new ideas of equivalence: one that works under all possible probability changes, and one that works if there is some change making them equivalent. They also provide efficient methods to find these equivalences and prove how hard it is to check them.
What this means in practice
- •For probabilistic model checkers: Reduce model size reliably when transition probabilities are uncertain but the structure is known, improving verification efficiency.
- •For systems engineers: Identify parts of uncertain probabilistic systems that behave equivalently under varying probabilities to simplify system analysis and design.
Authors
Syyeda Zainab Fatmi, Stefan Kiefer, James C. A. Main, David Parker
Abstract
Behavioural equivalences, such as language equivalence and probabilistic bisimilarity, are fundamental techniques for reducing the size of probabilistic models. However, these equivalences are sensitive to the precise values of transition probabilities, making them unsuitable in applications where probabilities are subject to approximation. Motivated by settings in which the support graph of a labelled Markov chain is known but the transition probabilities are uncertain, we study robust variants of these equivalences. We introduce universal (perturbation) equivalence, which captures a variant of equivalence that is resilient to all perturbations of transition probabilities: two states or distributions are universally equivalent if they remain equivalent under every assignment of transition probabilities consistent with the support graph. We also consider the dual notion of existential (perturbation) equivalence, which holds whenever there exists an assignment of transition probabilities that yields equivalence. We establish that, for states, universal language equivalence coincides with universal probabilistic bisimilarity and develop a characterisation that yields a polynomial-time partition refinement algorithm. We implement the algorithm and demonstrate experimentally that it is effective as a technique for robust model reduction. We further show that universal language equivalence for distributions is closely related to the state case, and prove NL-completeness of deciding universal equivalence for both states and distributions. We prove that, for states, existential language equivalence coincides with existential probabilistic bisimilarity and deterministic witness transition functions always suffice, leading to an NP-completeness result. In contrast, we show that existential language equivalence for distributions is complete for the existential theory of the reals.