Stutter bisimulation
સૈદ્ધાંતિક કોમ્પ્યુટર વિજ્ઞાનમાં, સ્ટટર બાયસિમ્યુલેશનને સહચાલક રીતે વ્યાખ્યાયિત કરવામાં આવે છે, જેમ કે બાયસિમ્યુલેશન. ધારો કે ટી. એસ. = (એસ, એક્ટ, →, આઇ, એપી, એલ) એક સંક્રમણ પ્રણાલી છે. ટી. એસ. માટે સ્ટટર બાયસિમ્યુલેશન એ S પર દ્વિસંગી સંબંધ R છે જેમ કે બધા માટે (s1, s2) જે R: L (s1) = L (s2) માં છે. જો s1 'એ પોસ્ટ (s1) માં હોય અને (s1', s2) એ R માં ન હોય, તો ત્યાં એક મર્યાદિત માર્ગ ટુકડો અસ્તિત્વમાં છે s2u1.uns2 'n ≤ 0 સાથે અને (s1, ui) એ R માં છે, અને (s1', s2 ') R માં છે. જો s2' એ પોસ્ટ (s2) માં હોય અને (s1, s2 ') એ R માં ન હોય, તો ત્યાં એક મર્યાદિત માર્ગ ટુકડો s1v1.vns1' n ≤ 0 સાથે અસ્તિત્વમાં છે અને (vi, s2) એ R માં છે, અને (s1 ', s2') સંદર્ભ સંક્રમણ પ્રણાલીમાં છે.