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.

翻译：暂无翻译