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'$.
Consider a language L without recursion. A different definition of a congruence ~ requires for any $n$-ary operator $f$ of L that
$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.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 ~.
Implementation:
(R_{1} | R_{2})\$\{$handover$\}$ where
R_{1} = start.handover.0
R_{2} = handover.finish.0
P --a--> P'
------------------------ (for P' != 0) P;Q --a--> P';Q |
P --a--> 0
---------------- P;Q --a--> Q |
In (a) and (b) 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.
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.
Click on 'portfolio' in the homework interface, and select for each of your submitted homeworks 1-10 whether or not you want to include it in your portfolio. The intention is that you select all homeworks except for one odd-numbered one and one even-numbered one, but in exceptional cases you are better off making a different selection. Your grade is calculated as $n/m$, where $n$ is the total number of points you got for the homeworks in your portfolio, and $m$ is the maximal number of points you could have gotten for the homeworks in your portfolio. However, to prevent you from including too few homeworks, $m$ will never be lower than 235, which is the total points of all homeworks 1-10, except for the most expensive odd-numbered homework, and the most expensive even-numbered homework.
This homework question is is about a mutual exclusion algorithm.
The algorithm deals with two concurrent processes A and B that want to alternate critical and noncritical sections. Each of these processes will stay only a ﬁnite amount of time in its critical section, although it is allowed to stay forever in its noncritical section. It starts in its noncritical section. The purpose of the algorithm is to ensure that they are never simultaneously in the critical section, and to guarantee that both processes keep making progress. $\newcommand{\rA}{{\it readyA}} \newcommand{\rB}{{\it readyB}} \newcommand{\tu}{{\it turn}} \newcommand{\tr}{{\it true}} \newcommand{\fa}{{\it false}} \newcommand{\procA}{{\rm A}} \newcommand{\procB}{{\rm B}}$
The processes use three variables. The Boolean variable $\rA$ can be written by process A and read by process B, whereas $\rB$ can be written by B and read by A. By setting $\rA$ to $\tr$, process A signals to process B that it wants to enter the critical section. The variable $\tu$ is a shared variable: it can be written and read by both processes. Initially $\rA$ and $\rB$ are both $\fa$ and $\tu = A$.
$\begin{array}{@{}l@{}} \underline{\bf Process~\procA}\\[.5ex] {\bf repeat~forever}\\ \left\{\begin{array}{ll} \ell_1 & {\bf noncritical~section}\\ \ell_2 & \it \rA := \tr \\ \ell_3 & \it \tu := B \\ \ell_4 & {\bf await}\,(\it \rB = \fa \vee \tu = A) \\ \ell_5 & {\bf critical~section}\\ \ell_6 & \it \rA := \fa\\ \end{array}\right. \end{array} ~~~~~ \begin{array}{@{}l@{}} \underline{\bf Process~\procB}\\[.5ex] {\bf repeat~forever}\\ \left\{\begin{array}{ll} m_1 & {\bf noncritical~section}\\ m_2 & \it \rB := \tr \\ m_3 & \it \tu := A \\ m_4 & {\bf await}\,(\rA = \fa \vee \tu = B) \\ m_5 & {\bf critical~section}\\ m_6 & \it \rB := \fa \\ \end{array}\right. \end{array}$
Model this protocol (including processes A and B and the three variables) as a Petri net. You may use actions like CritA and NonCritB; the actions that manipulate variables can all be labelled $\tau$. Hint: You may wish to introduce a place for each of the two values of a Boolean variable.
{$ab, acd, adc, a[cd]$}
Here $[cd]$ denotes the multiset containing c and d one time each.Rob van Glabbeek | notes | Rob.van.Glabbeek@ed.ac.uk |