# Difference between revisions of "Behavioural Equivalence"

(Created page with "<definition id="behavioural-equivalence"> Suppose that '''C''' is a category with pullbacks and <math>F : \mathbf{C} \to \mathbf{C}</math> a functor. Let <math>c : X \to F X...") |
m |
||

Line 1: | Line 1: | ||

<definition id="behavioural-equivalence"> | <definition id="behavioural-equivalence"> | ||

− | Suppose that '''C''' is a category with pullbacks and <math>F : \mathbf{C} \to \mathbf{C}</math> a functor. Let <math>c : X \to F X</math> and <math>d : Y \to F Y</math> be coalgebras in '''C'''. If there is a cospan <math>(X, c) \xrightarrow{h_1} (Z, e) \xleftarrow{h_2} (Y, d)</math> in <math>\mathrm{Coalg}(F)</math>, then we say that the pullback <math>h_1 \times_Z h_2</math> is a ''behavioural equivalence'' or ''kernel bisimulation'' for c and d. | + | Suppose that '''C''' is a category with [http://ncatlab.org/nlab/show/pullback pullbacks] and <math>F : \mathbf{C} \to \mathbf{C}</math> a functor. Let <math>c : X \to F X</math> and <math>d : Y \to F Y</math> be coalgebras in '''C'''. If there is a cospan <math>(X, c) \xrightarrow{h_1} (Z, e) \xleftarrow{h_2} (Y, d)</math> in <math>\mathrm{Coalg}(F)</math>, then we say that the pullback <math>h_1 \times_Z h_2</math> is a ''behavioural equivalence'' or ''kernel bisimulation'' for c and d. |

</definition> | </definition> | ||

## Latest revision as of 07:54, 26 February 2015

<definition id="behavioural-equivalence">

Suppose thatCis a category with pullbacks and a functor. Let and be coalgebras inC. If there is a cospan in , then we say that the pullback is abehavioural equivalenceorkernel bisimulationfor c and d.

</definition>

TODO:

- Compare to bisimilary and other notions. See
^{[1]}

## References[edit]

- ↑ Sam Staton, Relating Coalgebraic Notions of Bisimulation.