Stutter bisimulation
Stutter bisimulation is defined in a coinductive manner, as 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.
Link from a Wikipage to another Wikipage
primaryTopic
Stutter bisimulation
Stutter bisimulation is defined in a coinductive manner, as 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.
has abstract
Stutter bisimulation is define ...... s in R, and (s1',s2') is in R.
@en
Wikipage page ID
30,403,056
page length (characters) of wiki page
Wikipage revision ID
981,880,277
Link from a Wikipage to another Wikipage
wikiPageUsesTemplate
subject
comment
Stutter bisimulation is define ...... s in R, and (s1',s2') is in R.
@en
label
Stutter bisimulation
@en