Saturday, May 26, 2012

Interleave and Skip

In the interleave expression, the Skip Process can't be run unless all processes in the interleave process becomes Skip.
Skip||a->Skip||b->Skip
For example, for above expression, it has two possible next steps, which is events {a,b},but the Skip cannot go.

The reason the operational semantics of sequential expression is defined as
P->(CompleteEvent)P'
-------------------------
P;Q->(tau)P';Q

and Skip process is defined as

--------------
Skip->(CompleteEvent)Stop

now let P=Skip||a->Skip||b->Skip
if P allows that Skip to go, all other expression will force to stop!


No comments: