Talk:Bisimulation

I think the definition is buggy. Bisimulation need not be an autorelation of the form (i.e. R ⊆ S × S). In fact it makes more sense to talk about bisimilarity R between two different labeled transition systems (P, A, ->) and (Q, B, ->) such that \forall (p,a,p') \in P \exists (q,b,q') \in Q such that pRq and p'Rq'. 164.164.104.166 13:18, 10 September 2007 (UTC)

The definition is buggy - probably someone deleted the second part of definition. 132.230.166.199 17:47, 30 November 2006 (UTC)

The definition is modelled in the same way of the definition of simulation preorder, is easy to build a system S builded from the union of the system you want to relate in bisimulation. read there--213.47.52.27 (talk) 23:43, 8 November 2009 (UTC)

Agree with all the above. Could someone please fix this definition of bisimulation to make it less confusing? Defining bisimulation over a single transition system doesn't match any intuitions or practical uses. Furthermore the explanation refers to "simulation" further on but never relates to the entry for a Simulation preorder — Preceding unsigned comment added by Houseofwealth (talk • contribs) 20:33, 8 February 2019 (UTC)

Applications and algorithm equivalence

Are there any practical applications of bisimulation? It's not clear from the article whether bisimulation could be used to determine if two algorithms are equivalent. There is a related question here: http://wiki.riteme.site/wiki/Talk:Algorithm#Algorithm_equivalence_and_normal_forms pgr94 (talk) 16:55, 12 October 2011 (UTC)

Hi, yes. Many people use bisimulation to reason about when two programs give the same results, and also to reason about security protocols. It is a proof technique: to show that two programs are bisimilar, you just need to find a bisimulation. You can look at the work of Andy Gordon, Paul Levy and Eijiro Sumii, for example.

As for whether two algorithms are equivalent, it's very difficult to know what you mean by this. Do you just mean they compute the same results? if two algorithms are almost identical but one does things in a slightly different order, are they "equivalent"? ComputScientist (talk) 20:57, 12 October 2011 (UTC)

A more compact formulation

The current layout of the formulation looks awkward to read, but in fact it could be very compact. Also, it is more often to spell bisimulation without saying relation. I suggest using the following:

A bisimulation is a relation $R\subseteq S\times S$ over the state space $S$ such that if $p{\mathbin {R}}q$ then the following statements hold for any label $\alpha \in \Lambda$:

1. for every $p'$ with $p{\xrightarrow {\alpha }}p'$, there is $q'$ such that $q{\xrightarrow {\alpha }}q'$ and $p'{\mathbin {R}}q'$;

and conversely

2. for every $q'$ with $q{\xrightarrow {\alpha }}q'$, there is $p'$ such that $p{\xrightarrow {\alpha }}p'$ and $p'{\mathbin {R}}q'$.

— Preceding unsigned comment added by Xcycl (talk • contribs) 18:16, 1 April 2013 (UTC)