En la informática teórica , una bisimulación tartamudeo [1] se define en una coinductive manera, como es bisimulación .
Let TS = (S, Ley, →, I, AP, L) sea un sistema de transición . A bisimulación tartamudeo para TS es
una relación binaria R en S tal que para todo (s 1 , s 2 ) que está en R:
entonces existe un fragmento de camino finito s 2 u 1 …u n s 2 ' con n≥0 y
(s 1 ,u i ) está en R, y (s 1 ' ,s 2 ' ) está en R.
entonces existe un fragmento camino finito s 1 v 1 ... v n s 1 ' con n≥0 y
(v i , S 2 ) está en R, y (s 1 ' , s 2 ' ) está en R.