Editing Bisimulation (section)

== Variants of bisimulation ==
In special contexts the notion of bisimulation is sometimes refined by adding additional requirements or constraints. An example is that of [[stutter bisimulation]], in which one transition of one system may be matched with multiple transitions of the other, provided that the intermediate states are equivalent to the starting state ("stutters").<ref>{{cite book |last1=Baier |first1=Christel|author1-link= Christel Baier |last2=Katoen |first2=Joost-Pieter|author2-link=Joost-Pieter Katoen |title=[[Principles of Model Checking]] |date=2008 |publisher=MIT Press |isbn=978-0-262-02649-9 |page=527}}</ref>

A different variant applies if the state transition system includes a notion of ''silent'' (or ''internal'') action, often denoted with <math>\tau</math>, i.e. actions that are not visible by external observers, then bisimulation can be relaxed to be ''weak bisimulation'', in which if two states <math>p</math> and <math>q</math> are bisimilar and there is some number of internal actions leading from <math>p</math> to some state <math>p'</math> then there must exist state <math>q'</math> such that there is some number (possibly zero) of internal actions leading from <math>q</math> to <math>q'</math>. A relation <math>\mathcal{R}</math> on processes is a weak bisimulation if the following holds (with <math>\mathcal{S} \in \{ \mathcal{R}, \mathcal{R}^{-1} \}</math>, and <math>a,\tau</math> being an observable and mute transition respectively):

<math display="block">\forall p, q. \quad (p,q) \in \mathcal{S} \Rightarrow p \stackrel{\tau}{\rightarrow} p' \Rightarrow \exists q' . \quad q \stackrel{\tau^\ast}{\rightarrow} q' \wedge (p',q') \in \mathcal{S} </math>
<math display="block">\forall p, q. \quad (p,q) \in \mathcal{S} \Rightarrow p \stackrel{a}{\rightarrow} p' \Rightarrow \exists q' . \quad q \stackrel{\tau^\ast a \tau^\ast}{\rightarrow} q' \wedge (p',q') \in \mathcal{S} </math>

This is closely related{{how|date=September 2023}} to the notion of bisimulation "[[up to]]" a relation.<ref name="Pous2005">{{cite journal |author=Damien Pous |title=Up-to techniques for weak bisimulation |journal=Proc. 32nd ICALP |series=[[Lecture Notes in Computer Science]] |volume=3580 |publisher=Springer Verlag |year=2005 |pages=730–741}}</ref>

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 (respectively bisimilarity) relationship depending on the context.