Stamningsbisimulering



Inom teoretisk datavetenskap definieras en stamningsbisimulering på ett koduktivt sätt, liksom bisimulering . Låt TS=(S,Act,→,I,AP,L) vara ett övergångssystem . En stamningsbisimulering för TS är en binär relation R på S så att för alla (s 1 ,s 2 ) som är i R:

  1. L(s1 ) = L(s2 ) .
  2. Om s 1 ' är i Post(s 1 ) med (s 1 ' ,s 2 ) inte är i R,


då finns det ett finit vägfragment s 2 u 1 …u n s 2 ' med n≥0 och (s 1 , ui ) är i R, och (s 1 ' , s 2 ' ) är i R.

  1. Om s 2 ' är i Post(s 2 ) med (s 1 ,s 2 ' ) inte är i R,


då finns det ett finit vägfragment s 1 v 1 …v n s 1 ' med n≥0 och ( vi ,s 2 ) är i R, och (s 1 ' , s 2 ' ) är i R.

Hämtad från " https://en.wikipedia.org/w/index.php?title=Stutter_bisimulation&oldid=1068729006 "