INFR10089/INFR11248 — 2024 | Main page | Lectures and handouts | Homework |
| Piazza | Notes | HW Submissions |
| 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 ~.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.
Implementation:
(R1 | R2)\$\{$handover$\}$ where
R1 = start.handover.0
R2 = handover.finish.0
| Rob van Glabbeek | main MCS page | notes | Rob.van.Glabbeek@ed.ac.uk |
