Jump to content

Stutter bisimulation

Add links
From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by 2a02:1812:110c:dc00:4993:8f90:ad74:25e2 (talk) at 21:07, 31 October 2021. The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

In theoretical computer science, a stutter bisimulation[1] is defined in a coinductive manner, as is bisimulation.
Let TS=(S,Act,→,I,AP,L) be a transition system. A stutter bisimulation for TS is
a binary relation R on S such that for all (s1,s2) which is in R:

  1. L(s1) = L(s2).
  2. If s1' is in Post(s1) with (s1',s2) is not in R,

then there exists a finite path fragment s2u1…uns2' with n≥0 and
(s1,ui) is in R, and (s1',s2') is in R.

  1. If s2' is in Post(s2) with (s1,s2') is not in R,

then there exists a finite path fragment s1v1…vns1' with n≥0 and
(vi,s2) is in R, and (s1',s2') is in R.

References

  1. ^ Principles of Model Checking , by Christel Baier and Joost-Pieter Katoen, The MIT Press, Cambridge, Massachusetts.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Stutter_bisimulation&oldid=1052919161"