a.(b+τ.c)+τ.a.d | a.(b+τ.c)+τ.a.d+a.b | a.(b+τ.c)+τ.a.d+a.c | a.(b+τ.c)+τ.a.d+a.d |
This exercise is taken from Bayer/Katoen "Principles of Model Checking"
P ~_{L} Q if and only if C[P] ~ C[Q] for any L-context C[ ].
Prove that ~_{L} is the coarsest congruence finer than ~.normal progress | for | a.b.0 |
fair divergence | for | a.Δb.0 |
livelock | for | a.(b.0+ τ.Δ.0) |
deadlock | for | a.(b.0 + τ.0) |
Modify the definition of weak completed trace semantics in six different ways, namely such that
{ab, acd, adc, a[cd]}
Here [cd] denotes the multiset containing c and d one time each.The purpose of the algorithm is to ensure that Processes $A$ and $B$ are never simultaneously in the critical section, and to guarantee that both processes keep making progress. It is correct if these requirements are met.
Rob van Glabbeek | notes | rvg@cse.unsw.edu.au |