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 |
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 |
Give a counterexample, showing that they are not always isomorphic.
The most difficult one is to define PT(<X | X=E>). It will be the least fixpoint of some operator. Which one? Explain why such a least fixpoint always exists.
x --a--> x'
------------------ (for x' != 0) x;y --a--> x';y |
x --a--> 0
------------ x;y --a--> y |
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 ~.$P_i \sim Q_i$ for $i=1,...,n$ implies $f(P_1,...,P_n)\sim f(Q_1,...,Q_n)$.
Show that this definition is equivalent to the one above.Let $B$ be a 1-bit buffer, specified as follows: \[ B_{\varepsilon} = \sum_{d \in Data} r(d).B_d \] \[ B_{d} = s(d).B_\varepsilon \]
{ab, acd, adc, a[cd]}
Here [cd] denotes the multiset containing c and d one time each.Does this formula hold for Peterson's protocol (under the same translation η from process graphs to Kripke structures we have been using in class)? Explain why this is the case or describe a run of the protocol that forms a counterexample.
Does this formula hold for Peterson's protocol? Explain why this is the case or describe a run of the protocol that forms a counterexample.
Does this formula hold for Peterson's protocol? Explain why this is the case or describe a run of the protocol that forms a counterexample.
Now give an example $(P,B,F,\phi)$ such that $P \models_B^F \phi$, but not $P \models_\emptyset^F \phi$ and not $P \models_B \phi$.
Client A and Interface A communicate through 3 shared actions:
$r_A$ is a request by the client to the interface to enter the critical section;
$g_A$ is a signal from the interface to the client, allowing entry to the critical
section -- $g$ stands for "granting the request";
$e_A$ is a signal from the client to the interface, saying it is exiting the critical
section.
We assume the clients are well behaved. This means:
Client $i$ (where $i\in\{A,B\}$) will engage in the actions $r_i$, $g_i$ and $e_i$ only in
this order (looping back to $r_i$ after $e_i$).
Whenever client $i$ gets permission to enter ($g_i$), it will, after a finite period of time,
leave the critical section and signal this by sending the signal $e_i$.
When the interface performs the action $g_i$, it cannot be blocked by the client.
There is no obligation for a client to ever do $r_i$.
Rob van Glabbeek | notes | rvg@cse.unsw.edu.au |