Bisimulation through Probabilistic Testing

By Kim Guldstrand Larsen, A. Skou. 1991

Abstract We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm can distinguish, with a probability arbitrarily close to one, between processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2 3 - bisimulation —which lies strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify a new process relation called probabilistic bisimulation—which is strictly stronger than bisimulation.

How researchers see this paper

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

Citations in the corpus

Advanced Probabilistic Couplings for Differential Privacy (2016, neutral): “There are seemingly few applications of coupling in formal veriﬁcation, despite considerable research on probabilistic bisimulation (ﬁrst introduced by Larsen and Skou [33]) and probabilistic relational program logics (ﬁrst introduced by Barthe et al. [4]).”
Proving Differential Privacy via Probabilistic Couplings (2016, neutral): “There are seemingly few applications of coupling in formal veriﬁcation, despite considerable research on probabilistic bisimulation (ﬁrst introduced by Larsen and Skou [23]) and probabilistic relational program logics (ﬁrst introduced by Barthe et al. [3]).”
Metrics for Finite Markov Decision Processes (2004, background): “Bisimulation was introduced by Larsen and Skou (1991) based on ideas of Park (1981) and Milner (1980).”
Value Preserving State-Action Abstractions (2020, methodology): “Later, Dean and Givan (1997) developed a method for finding states that behave similarly to one another via the bisimulation property (Larsen and Skou, 1991).”
Universal coalgebra: a theory of systems (2000, background): “1 This type of bisimulation seems to be underlying many of the recently proposed probabilistic bisimulations [46, 85].”
Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation (2011, background): “, for each state and for each action, there exists at most one outgoing transition from the state), probabilistic bisimulations can be characterised by simpler forms of logics, as observed in [37, 16, 49].”
Metrics for labelled Markov processes (2004, methodology): “A representative sample of such work are the following papers: [HJ90, JY95, LS91 , HS86, BBS95, vGSS95, CSZ92].”
An algebraic approach to abstraction in reinforcement learning (2004, background): “Minimization approaches for other modeling paradigms, such as probabilistic automata (Paz, 1971) and probabilistic transition systems (Larsen and Skou, 1991), are usually based on the notion of bisimulation and its stochastic extension.”
Bisimulation Metrics for Continuous Markov Decision Processes (2011, methodology): “Larsen and Skou [41] extended the notion of bisimulation to a probabilistic framework.”
Language-based information-flow security (2003, background): “Sabelfeld and Sands [11] connect probabilistic security with probabilistic bisimulation[105] which is a standard semantic model for probabilistic computation.”
Bounding Performance Loss in Approximate MDP Homomorphisms (2008, methodology): “Bisimulation is a well-known, well-studied notion of behavioral equivalence between systems (Larsen & Skou, 1991; Milner, 1995) which has been specialized for MDPs by Givan et al (2003).”
Representation Discovery for MDPs Using Bisimulation Metrics (2015, background): “Probabilistic bisimulation is an equivalence relation between states of a process due to Larsen and Skou (1991).”
Probabilistic Extensions of Process Algebras (2001, methodology): “2 This de nition occurs with minor variations in [55,57, 31, 38,52, 51, 41].”