| 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 |
if $P \mathrel{\mathcal{B}} Q$ and $P \stackrel{\alpha}\longrightarrow P'$,
then there are $Q_0$, $Q_1$, ... , $Q_n$ for some $n \geq 0$,
and $Q'_0$, $Q'_1$, ... , $Q'_m$ for some $m \geq 0$
such that
$Q=Q_0 \stackrel{\tau}\longrightarrow Q_1 \stackrel{\tau}\longrightarrow \dots
\stackrel{\tau}\longrightarrow Q_n \stackrel{(\alpha)}\longrightarrow Q'_0
\stackrel{\tau}\longrightarrow Q'_1 \stackrel{\tau}\longrightarrow \dots
\stackrel{\tau}\longrightarrow Q'_m$,
and moreover $P \mathrel{\mathcal{B}} Q_i$ for all $i=1,...,n$
and $P' \mathrel{\mathcal{B}} Q'_j$ for all $j=0,...,m$.
if $P \mathrel{\mathcal{B}} Q$ and $P \stackrel{\alpha}\longrightarrow P'$,
then there are $Q_0$, $Q_1$, ... , $Q_n$ for some $n \geq 0$,
such that
$Q=Q_0 \stackrel{\tau}\longrightarrow Q_1 \stackrel{\tau}\longrightarrow \dots
\stackrel{\tau}\longrightarrow Q_n \stackrel{(\alpha)}\longrightarrow Q'$,
and moreover $P \mathrel{\mathcal{B}} Q_n$ and $P' \mathrel{\mathcal{B}} Q'$.
Give a counterexample, showing that they are not always isomorphic.
In (c) and (d) below, work with a form of LTS in which any state (possibly with outgoing transitions) can have the label $\surd$. Moreover, the label $\surd$ can occur in a (partial or completed) trace, as explained in the notes.
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.
Implementation:
(R1 | R2)\$\{$handover$\}$ where
R1 = start.handover.0
R2 = handover.finish.0
|
x --a--> x'
------------------ (for x' != 0) x;y --a--> x';y |
x --a--> 0
------------ x;y --a--> y |
On Monday 13-7-2020 at 15:15 there will be a seminar presentation on Zoom.
Anything mentioned in these seminar presentations will be seen as
material treated in class, on which exam questions may be asked.
So if you have questions about them, ask them to the presenter at the
end of the zoom lecture (or during if they are urgent for continuous understanding).
We assume such an algorithm to be modelled as a Kripke structure.
Among the atomic propositions that label the states of this Kripke
structure is IntentA, saying that Process A wants to enter
the critical section, but has not done so yet. We also have an
atomic proposition CritA, stating that Process A is in its
critical section. Likewise we have atomic propositions IntentB and CritB.
{ab, acd, adc, a[cd]}
The correct answer as to where IntendA should hold is
disputed in academic circles. Many people, especially ones that like
to formally verify Peterson's algorithm by means of process algebra,
claim that it holds for states $\ell_3$, $\ell_4$ and $\ell_5$ only.
The argument is that the intention to enter the critical section
occurs when the process speaks up about it, by performing the action readyA := true.
But some say that a better model is
obtained by additionally including $\ell_2$ in IntendA.
The students in this class that answered Q3 were evenly divided
between including $\ell_2$ or not.
Of course, full points were available for both points of view.
Please answer HW12 Q3 parts (c) and (d) again, but now starting from the
opposite postulate on whether IntendA holds in $\ell_2$
compared to your previous answer.
Client A and Interface A communicate through 3 shared actions:
We assume the clients are well behaved. This means:
Now consider the process algebra CCS upgraded with timeout actions ${\rm t}.\!P$.
The operational semantics is exactly the same as for every other action prefixing operator $\alpha.\!P$.
It yields a transition $\stackrel{\rm t}{\longrightarrow}$.
The passage of time is modelled in the following way.
When a system arrives in a state $P$, and at that time $X$ is the set of actions allowed by the
environment, there are two possibilities.
If $P$ has an outgoing transition $P \stackrel\alpha\longrightarrow Q$ with $\alpha \in X\cup \{\tau\}$,
the system immediately takes one of the outgoing transitions $P \stackrel\alpha \longrightarrow Q$ with $\alpha \in X\cup \{\tau\}$,
without spending any time in state $P$. The choice between these actions is entirely nondeterministic.
The system cannot immediately take a transition $\stackrel b\longrightarrow$ with $b\in A{\setminus}X$, because the
action $b$ is blocked by the environment. Neither can it immediately take a transition $P\stackrel{\rm t}\longrightarrow Q$,
because such transitions model the end of an activity with a finite but positive duration that
started when reaching state $P$.
In case $P$ has no outgoing transition $P \stackrel\alpha\longrightarrow Q$ with $\alpha \in X\cup \{\tau\}$,
the system idles in state $P$ for a positive amount of time. This idling can end in two possible ways.
Either one of the time-out transitions $P \stackrel{\rm t}\longrightarrow Q$ occurs, or the environment spontaneously
changes the set of actions it allows into a different set $Y$ with the property that
$P \stackrel a\longrightarrow Q$ for some $a \in Y$. In the latter case a transition $P \stackrel a\longrightarrow Q$ occurs, with $a \in Y$.
The choice between the various ways to end a period of idling is entirely nondeterministic.
It is possible to stay forever in state $P$ only if there are no outgoing time-out transitions $P \stackrel{\rm t}\longrightarrow Q$.
A crucial law that is valid in this setting is $\tau.P + {\rm t}.Q = \tau.P$.
As I told in lecture 16, Peterson's Protocol can be made to satisfy the liveness property, by
inserting a t-action between entering and leaving the critical section.
Consider a mutual exclusion protocol $ME$ with as visible actions
${\it en}_A$,
${\it ln}_A$,
${\it en}_B$,
${\it ln}_B$,
${\it ec}_A$,
${\it lc}_A$,
${\it ec}_B$ and
${\it lc}_B$.
They represent entering and leaving the non-critical and critical
sections of processes A and B. All other transitions are $\tau$'s.
As in HW14 Q3, our protocol merely models an interface; the process A and B that really engage in
critical and noncritical sections are specified by
PrA := (noncritical stuff).${\it ln}_A$${\it
ec}_A$.(critical stuff).${\it lc}_A$.${\it en}_A$.PrA
The goal of this exercise is to arrive at a sound and complete list of requirements for $ME$,
each of which has the form $ME \models^C_B \phi$ for a completeness criterion $C$, a set of visible
actions $B$, and an LTL formula $\phi$. The criterion is sound if it is satisfied by a decent mutual
exclusion protocol (such as the one mentioned in the previous question). The list is complete, if
it is not satisfied by systems that should not be regarded as correct mutual exclusion protocols.
The closer your list is to complete, the more of these non-ME systems it rules out.
The mode of delivery for this exercise is a bit different then usual. Rather then using the homework
interface, we invite you to post your contributions to Piazza, so that it is visible to the entire
class at once. We can imagine a blue team and a red team; you can be a member of either or both, and
may switch allegiances when you want.
As a member of the blue team you can add a requirement to list
of requirements posted so far. List the previously posted set of requirements you agree with, and
then your addition. It is worth credit if your requirement is sound, and rules out at least one
more non-ME systems.
As a member of the red team, you establish the non-completeness of the requirements posted so far,
by proposing a system that satisfies the posted requirements, yet is not a correct mutual exclusion protocol.
Please list in your post the posted requirements satisfied by your solution.
Part of the game is to take the letter rather then the spirit of the requirements.
So you system might be one that satisfies the requirements as posted, yet is clearly unintended.
Instead of this you may also undermine a posted requirement by arguing that it is too strong and
will not be satisfied by any correct mutual exclusion algorithm.
For this exercise you can assume the existence of a data structure [Int], which represents a queue
of integers (e.g. [1,5,7,2,3]). The empty list is denoted by [ ]. Without further definition you can
use the standard (partial) functions head, tail, and append that return the
"oldest" element in the queue, remove the "oldest" element, and add an integer to the queue, respectively.
Examples are
head([1,5,7,2,3]) = 1Homework 10, Monday 13-7-2020: CTL and LTL
(HW 10 and 11 are
due on 18-7-2020 at 5pm; accepted without penalty until 20-7-2020 at 10am)
15-7-2020: Oops, what I mean to ask was:
Give a CTL-X formula that shows the difference
between the processes b+τ.(a+b) and b+a+τ.(a+b), or
show that there isn't any.
At this time you are free to answer either
version (or both). But tell me which one.
Homework 11, Tuesday 14-7-2020: Partition refinement
Homework 12, Monday 20-7-2020
(HW 12 and 13 are due on 25-7-2020 at 5pm; accepted without penalty until 27-7-2020 at 10am)
Homework 13, Tuesday 21-7-2020: Petri nets and non-interleaving semantics
The communication function is given by γ(b,d)=a.
Moreover, the choice between b and c should be made only
after execution of a.
Course evaluation
Please fill in the
course and instructor evaluation forms.
Homework 14, Monday 27-7-2020
The correct answer to HW12, Q3a is that CritA holds in all
states with the label $\ell_6$. Namely the state $\ell_5$ is
by definition the state right before the
action ${\it ec}_A$ takes place; hence the
process is not yet in its critical section. However, I gave full
points to people who put $\ell_5$ in the critical section as well.
$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.
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$.
A good way to do this is to propose a number of algebraic laws like
$\neg \textbf{F}\phi = \textbf{G} \neg \phi$, and prove each of
them correct by showing that, on arbitrary paths in arbitrary
Kripke structures, the left-hand side is valid iff the right-hand
side is valid. This involves the definition of the modalities involved.
Then obtain the requested equivalences by combining those algebraic laws.
Homework 15, Tuesday 28-7-2020
Practice exam
Here is the final exam I gave when I taught this
course at a previous occasion. It should give a good indication of
what kind of questions (how many and how hard) to expect.
Note: Question 2(d) covers material encountered during a student presentation.
It is not covered this year. We also didn't cover Q4(f). All the rest is covered.
Homework 16, Monday 3-8-2020: Fair schedulers and mutual exclusion
(HW16 Q1 and HW17 are due on 7-9-2020 at 5pm; accepted without penalty until 7-10-2020 at 10am.
The answers may be revealed in the last class, which is on Zoom on Monday 7-10-2020 at 3pm.)
Homework 17, Tuesday 4-8-2020: Value-passing process algebra
tail([1,5,7,2,3]) = [5,7,2,3]
append(17,[1,5,7,2,3]) = [1,5,7,2,3,17]
| Rob van Glabbeek | notes | rvg@cse.unsw.edu.au |