Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation

By Yuxin Deng, Wenjie Du. 2011

34 citations recorded by the source corpus.

Many behavioural equivalences or preorders for probabilistic processes involve a lifting operation that turns a relation on states into a relation on distributions of states. We show that several existing proposals for lifting relations can be reconciled to be different presentations of essentially the same lifting operation. More interestingly, this lifting operation nicely corresponds to the Kantorovich metric, a fundamental concept used in mathematics to lift a metric on states to a metric on distributions of states, besides the fact the lifting operation is related to the maximum flow problem in optimisation theory. The lifting operation yields a neat notion of probabilistic bisimulation, for which we provide logical, metric, and algorithmic characterisations. Specifically, we extend the Hennessy-Milner logic and the modal mu-calculus with a new modality, resulting in an adequate and an expressive logic for probabilistic bisimilarity, respectively. The correspondence of the lifting operation and the Kantorovich metric leads to a natural characterisation of bisimulations as pseudometrics which are post-fixed points of a monotone function. We also present an “on the fly” algorithm to check if two states in a finitary system are related by probabilistic bisimilarity, exploiting the close relationship between the lifting operation and the maximum flow problem.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Proving Differential Privacy via Probabilistic Couplings (2016, neutral): “…researchers have developed a wide variety of tools for reasoning about probabilistic liftings, explored applications in numerous areas including security and biology, and uncovered deep connections with the Kantorovich metric and the theory of optimal transport (for a survey, see Deng and Du [11]).”
Verified Computational Differential Privacy with Applications to Smart Metering (2013, background): “The scale parameter α = exp( /Δ) of the distribution is chosen to offer -differential privacy on the basis of the sensitivity of a single reading being Δ, an upper bound on the maximum possible value of wiri,t.”
Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs (2013, background): “Moreover, Lemma 6 extends a previous result in [14] about the equivalence between the exact liftings of [15] and [19] to the approximate setting.”
Relational Reasoning via Probabilistic Coupling (2015, background): “Deng and Du [6] provide an excellent introductory exposition to lifting, and give several equivalent characterizations of lifting, including an inductive definition and a definition based on maximal flows.”