Difference between revisions of "Behavioural Equivalence"

From cLab
Jump to: navigation, search
(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 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.

</definition>

TODO:

  • Compare to bisimilary and other notions. See [1]

References[edit]

  1. Sam Staton, Relating Coalgebraic Notions of Bisimulation.