Papers for

probabilistic model checkers

Papers whose findings have a practical use for this group, as judged from the abstract. Open a paper to read what it means in practice.

Perturbation resilient equivalences reduce uncertain probabilistic models

Perturbation equivalence in labelled Markov chains

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.

Fri 11 SeptLogic in Computer ScienceFormal Languages and Automata Theory
The gist
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.
Open → 2609.13401v1