Bisimulation

Bisimulation

In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa.

Intuitively two systems are bisimilar if they match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer.

Formal definition

Given a labelled state transition system (S, Λ, →), a "bisimulation" relation is a binary relation R over S (i.e., R ⊆ S × S) such that both R-1 and R are simulations.

Equivalently R is a bisimulation if for every pair of elements p, q in S with (p,q) in R, for all α in Λ:

for all p' in S,

:: p overset{alpha}{ ightarrow} p'

:implies that there is a q' in S such that

:: q overset{alpha}{ ightarrow} q'

:and (p',q') in R;

and, symmetrically, for all q' in S

::q overset{alpha}{ ightarrow} q'

:implies that there is a p' in S such that

::p overset{alpha}{ ightarrow} p'

:and (p',q') in R.

Given two states p and q in S, p is bisimilar to q, written p , sim , q, if there is a bisimulation R such that (p, q) is in R.

The bisimilarity relation , sim , is an equivalence relation. Furthermore, it is the largest bisimulation relation over a given transition system.

Note that it is not always the case that if p simulates q and q simulates p then they are bisimilar. For p and q to be bisimilar, the simulation between p and q must be the inverse of the simulation between q and p. Counter-example (in CCS, describing a coffee machine) : M=p.overline{c}.M+p.overline{t}.M+p.(overline{c}.M+overline{t}.M) and M'=p.(overline{c}M'+overline{t}M') simulate each other but are not bisimilar.

Alternative definitions

Relational definition

Bisimulation can be defined in terms of composition of relations as follows.

Given a labelled state transition system (S, Λ, →), a "bisimulation" relation is a binary relation R over S (i.e., R ⊆ S × S) such that

::R ; overset{alpha}{ ightarrow}quad {subseteq}quad overset{alpha}{ ightarrow} ; R:and::R^{-1} ; overset{alpha}{ ightarrow}quad {subseteq}quad overset{alpha}{ ightarrow} ; R^{-1}

Fixpoint definition

Bisimilarity can also be defined in order theoretical fashion, in terms of fixpoint theory, more precisely as the greatest fixed point of a certain function defined below.

Given a labelled state transition system (S, Λ, →), define F:mathcal{P}(S imes S) o mathcal{P}(S imes S) to be a function from binary relations over S to binary relations over S, as follows:

Let R be any binary relation over S. F(R) is defined to be the set of all pairs (p,q) in S × S such that:

:forall alpha in Lambda. , forall p' in S. ,p overset{alpha}{ ightarrow} p' , Rightarrow , exists q' in S. , q overset{alpha}{ ightarrow} q' , extrm{ and }, (p',q') in R

and

:forall alpha in Lambda. , forall q' in S. ,q overset{alpha}{ ightarrow} q' , Rightarrow , exists p' in S. , p overset{alpha}{ ightarrow} p' , extrm{ and }, (p',q') in R

Bisimilarity is then defined to be the greatest fixed point of F.

Game theoretical definition

Bisimulation can also be thought of in terms of a game between two players: attacker and defender.

"Attacker" goes first and may choose any valid transition, alpha, from (p,q). I.e.:

(p,q) overset{alpha}{ ightarrow} (p',q) or (p,q) overset{alpha}{ ightarrow} (p,q')

The "Defender" must then attempt to match that transition, alpha from either (p',q) or (p,q') depending on the attacker's move.I.e., they must find an alpha such that:

(p',q) overset{alpha}{ ightarrow} (p',q') or (p,q') overset{alpha}{ ightarrow} (p',q')

Attacker and defender continue to take alternating turns until:

* The defender is unable to find any valid transitions to match the attacker's move. In this case the attacker wins.
* The game reaches states (p,q) which are both 'dead' (i.e., there are no transitions from either state) In this case the defender wins
* The game goes on forever, in which case the defender wins.
* The game reaches states (p,q), which have already been visited. This is equivalent to an infinite play and counts as a win for the defender.

By the above definition the system is a bisimulation if and only if there exists a winning strategy for the defender.

Variants of bisimulation

In special contexts the notion of bisimulation is sometimes refined by adding additional requirements or constraints. For example if the state transition system includes a notion of "silent" (or "internal") action, often denoted with τ, i.e. actions which are not visible by external observers, then bisimulation can be relaxed to be "weak bisimulation", in which if two states p and q are bisimilar and there is some number of internal actions leading from p to some state p' then there must exist state q' such that there is some number (possibly zero) of internal actions leading from q to q'.

Typically, if the state transition system gives the operational semantics of a programming language, then the precise definition of bisimulation will be specific to the restrictions of the programming language. Therefore, in general, there may be more than one kind of bisimulation, (bisimilarity resp.) relationship depending on the context.

Bisimulation and modal logic

Since Kripke models are a special case of (labelled) state transition systems, bisimulation is also a topic in modal logic. In fact, modal logic is the fragment of first-order logic invariant under bisimulation (Van Benthem's theorem).

See also

* Operational semantics
* State transition systems
* Simulation preorder
* Congruence relation

Software tools

* [http://www.inrialpes.fr/vasy/cadp CADP - tools to minimize and compare finite-state systems according to various bisimulations]

References

# cite conference
first = David
last = Park
year = 1981
title = Concurrency and Automata on Infinite Sequences.
conference = Proceedings of the 5th GI-Conference Karlsruhe.
booktitle = Theoretical Computer Science.
series = Lecture Notes in Computer Science.
editor = Deussen, P. (ed.)
pages = 167–183
volume = 104
publisher = Springer-Verlag
id = ISBN 978-3-540-10576-3

# cite book
last = Milner
first = Robin
title = Communication and Concurrency.
year = 1989
publisher = Prentice Hall
isbn = 0-13-114984-9


Wikimedia Foundation. 2010.

Игры ⚽ Поможем решить контрольную работу

Look at other dictionaries:

  • Bisimulation — En informatique théorique une bisimulation est une relation binaire entre systèmes de transition d états, associant les systèmes qui se comportent de la même façon au sens qu un des systèmes simule l autre et vice versa. Une bisimulation sur un… …   Wikipédia en Français

  • Bisimulation — In der theoretischen Informatik ist eine Bisimulation eine Relation zwischen den Zuständen eines Transitionssystems, die solche Zustände miteinander in Beziehung setzt, die sich gleich verhalten. Das bedeutet, dass der eine Zustand die Übergänge… …   Deutsch Wikipedia

  • bisimulation — noun an equivalence relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice versa See Also: bisimilar, simulation preorder …   Wiktionary

  • Probabilistic bisimulation — is an extension of the concept of bisimulation for fully probabilistic transition systems.A discrete probabilistic transition system is a triple S = (St,Act, au:St imes Act imes St ightarrow [0,1] ) where au(s,a,t) gives the probability of… …   Wikipedia

  • π-calculus — In theoretical computer science, the π calculus (or pi calculus) is a process calculus originally developed by Robin Milner, Joachim Parrow and David Walker as a continuation of work on the process calculus CCS (Calculus of Communicating Systems) …   Wikipedia

  • Pi-calculus — In theoretical computer science, the pi calculus is a process calculus originally developed by Robin Milner, Joachim Parrow and David Walker as a continuation of work on the process calculus CCS (Calculus of Communicating Systems). The aim of the …   Wikipedia

  • Stuttering equivalence — In theoretical computer science, stuttering equivalence, a relation written as:pisim {st}pi , can be seen as a partitioning of path pi and pi into blocks, so that states in the k^{mathrm{th block of one path are labeled (L(sdot)) the same as… …   Wikipedia

  • Semantique de Kripke — Sémantique de Kripke La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à… …   Wikipédia en Français

  • Sémantique de Kripke — La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à dire que le modèle qui… …   Wikipédia en Français

  • Sémantique de kripke — La sémantique de Kripke a été proposée par Saul Aaron Kripke et est la sémantique traditionnellement associée à la logique intuitionniste et aux logiques modales. Elle est fondée sur un univers de mondes possibles, c est à dire que le modèle qui… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”