## Homework 1, Tuesday 19-9-2023

(Due: 26-9-2023 at 10am; accepted without penalty until 27-9-2023 at 10am)

## Homework 2, Thursday 21-9-2023

(Also due: 26-9-2023 at 10am; accepted without penalty until 27-9-2023 at 10am)
1. Give an example of two processes that have the same partial traces but different completed traces. Moreover, the completed traces of the one should not be a subset of the completed traces of the other.
2. Give an example of a process that has no finite completed traces at all.
3. Give an example of two processes without infinite traces that are weakly completed trace equivalent and also strongly partial trace equivalent but not strongly completed trace equivalent.
4. [Harder; can be skipped by students that merely aim for a basic good grade.]
Consider a more bureaucratic version of the relay race that was presented in class. This time runner 1 may only pass the stick to runner 2 in the presence of a bureaucrat, who is stationed halfway the start and finish. The bureaucrat will watch the transaction and subsequently make a note of it in his notebook, that will be kept for posterity. Consider a specification that mentions the start of the race (start), the delivery of the parcel (finish) and the making of the bureaucratic note (note). Describe the specification and the implementation in ACP.

## Homework 3, Tuesday 26-9-2023: Linear time versus branching time

(Due: 3-10-2023 at 10am; accepted without penalty until 4-10-2023 at 10am)

## Homework 4, Thursday 28-9-2023

(Also due: 3-10-2023 at 10am; accepted without penalty until 4-10-2023 at 10am)
1. Let P be the process given by the recursive equation X = a.(b.X + c.X)
and Q be the process (c+e).a. Assume an ACP communication function γ given by γ(a,c)=γ(c,a)=d.
1. Draw a process graph representation of P and Q.
2. Draw a process graph representation of P||Q.
3. Draw a process graph representation of {a,c}(P||Q).
2. Consider a process called "gatekeeper" that makes sure that of 2 other processes "1" and "2", at most one is in its critical section. Its action are "hear request of process i to enter critical section", or h(i) for short; "admit process i into critical section", or a(i); and "observe that process i exits the critical section", e(i). Here i can have the values 1 or 2. Keep in mind that each of the processes i may enter the critical section multiple times. The actions h(i), a(i) and e(i) all synchronise with corresponding actions h(i), a(i) and e(i) from the processes 1 and 2. Processes 1 and 2 have the form P(i)=h(i).a(i).e(i).P(i). The gatekeeper should be able to hear (and remember) a request in any state. Deadlock should be avoided.
1. Draw a process graph describing the correct behaviour of the gatekeeper.
2. Express the behaviour of the gatekeeper by a system of recursive equations.

## Homework 5, pertaining to Tuesday 3-10-2023

(Due: 11-10-2023 at 10am; accepted without penalty until 12-10-2023 at 10am This is a day later than usual, because the homework was also posted later than usual.)
1. Describe the relay race in CCS in a similar way that the class notes describe it in ACP.
2. Give a CCS expression for the vending machine intended by Q2 of HW1. This involves declaring a recursive specification.
3. Prove that up to strong bisimilarity ACP$^{\tau\epsilon}_R$ is at least as expressive as CCS. Here ACP$^{\tau\epsilon}_R$ is ACP, enriched with the constants $\tau$ and $\epsilon$, to which relabelling operators have been added. This is done by supplying for each binary operator $f$ of CCS, an ACP$^{\tau\epsilon}_R$ expression $C[X,Y]$ with (free) variables $X$ and $Y$, such that the CCS expression $f(X,Y)$ is strongly bisimilar to the ACP$^{\tau\epsilon}_R$ expression $C[X,Y]$. The latter means that no matter which process graphs $G$ and $H$ you fill in for $X$ and $Y$, the process $f(G,H)$, which is a process graph obtained by applying the denotational semantics of the CCS operator $f$, is strongly bisimilar with the process graph $C[G,H]$ obtained by applying the denotational semantics of ACP$^{\tau\epsilon}_R$. An example of $f(X,Y)$ is the CCS parallel composition $X|Y$. The same should be done for the unary operators and constants of CCS, but then using 1 or 0 variables. Of course you have to choose the set of actions $A$ and the communication function $\gamma$ of ACP$^{\tau\epsilon}_R$ appropriately. Recall that $\gamma(a,b)$, if defined, must be a non-$\tau$ action.
4. Does the CCS recursive specification $Y = (b.Y | d.Y | e.Y)\backslash \{d\}$ have a unique solution up to strong bisimilarity? How do you know this?

## Homework 6, Thursday 5-10-2023

(Also due: 11-10-2023 at 10am; accepted without penalty until 12-10-2023 at 10am)

## Homework 7, Tuesday 10-10-2023

(Due: 17-10-2023 at 10am; accepted without penalty until 18-10-2023 at 10am)
1. Show that (strong, finitary) partial trace equivalence is a congruence for the CCS relabelling operator. This means that whenever P =CT Q and f: A -> A is a relabelling operator, it must be the case that P[f] =CT Q[f].
2. Use the axioms of CCS to proof by means of equational logic that $((a.(b+c.\bar{e})) \mid (e + \bar{b}.c))\backslash \{b,e\}$ is strongly bisimilar to $a.(c|\tau)$. Here the CCS constant $0$ is elided, meaning that we abbreviate $a.0$ to $a$. Moreover, $P\backslash\{b,e\}$ is the same as $P \backslash b \backslash e$. Which CCS law(s) for restriction do you need to show this?
3. Use RSP to show that the processes $X$ and $a.Y$, defined by $X=a.b.X$ and $Y = b.a.Y$ are strongly bisimilar.
4. [Fairly hard] An equivalence ~ is a congruence for a language L if P ~ Q implies that C[P] ~ C[Q] for every context C[ ]. Here a context C[ ] is an L-expression with a hole in it, and C[P] is the result of plugging in P for the hole.

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.
5. [Hard] (this goes beyond the normal load; only do this exercise if you want to be one of those exceptional students with marks $>$ 80/100)
The congruence closure ~L of ~ is defined by

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 ~.

## Homework 8, Thursday 12-10-2023

(Also due: 17-10-2023 at 10am; accepted without penalty until 18-10-2023 at 10am)
1. Consider the processes a.0 + b.0, τ.(a.0 + b.0), τ.a.0 + b.0, a.τ.0 + b.0 and τ.(a.0 + b.0) + a.0.
1. Which of these processes are weak bisimulation equivalent to each other, and why (or why not)?
2. Which of these processes are branching bisimulation equivalent to each other, and why (or why not)?
3. Which of these processes are rooted weak bisimulation equivalent to each other, and why (or why not)?
4. Which of these processes are rooted branching bisimulation equivalent to each other, and why (or why not)?
2. Recall the specification and implementation of the relay race in CCS (HW 4, Q3):

Specification:    start.finish.0

Implementation:    (R1 | R2)\$\{$handover$\}$    where
R1 = start.handover.0
R2 = handover.finish.0

Prove the rooted branching bisimulation equivalence between the specification and the implementation by means of equational logic, using the equational axiomatisation of CCS.

## Homework 9, Tuesday 17-10-2023

(Due: 24-10-2023 at 10am; accepted without penalty until 25-10-2023 at 10am)
1. Model the relay race in CSP.
2. How would you translate the CSP expressions (ab) ⊓ c and (ab) ☐ c into CCS? Here I omitted trailing .0's.
3. Sequencing is a binary operation defined on any process graphs; it starts with its second component as soon as its first component cannot do any further actions.
Sequential composition, on the other hand, is defined on process graphs equipped with a state-labelling, where some states are marked with the symbol for successful termination, ✔. Here the second component starts only when the first one successfully terminates. This is the operator that occurs in ACP.
1. Give a definition of sequencing as an operator on process graphs.
2. Give an example that shows the difference between these two operators.
3. Here is an attempted operational semantics of the sequencing operator:
 P --a--> P' ------------------------ (for P' != 0) P;Q --a--> P';Q P --a--> 0 ---------------- P;Q --a--> Q
Is it in GSOS format? What is wrong with this operational semantics? Show that strong bisimulation is not a congruence for the operator defined by these operational rules (in the context of CCS).

## Homework 10, Thursday 19-10-2023

(Also due: 24-10-2023 at 10am; accepted without penalty until 25-10-2023 at 10am)
1. In the paper available at https://www.cse.unsw.edu.au/~rvg/pub/spec1.pdf there are a number of pictures, called Counterexample 1, 2, 3, etc. For each of counterexamples 2 to 6, provide a HML formula (if needed with infinite conjunctions) that holds for the left process, but not for the right one.
2. Give an example of a process that satisfies the HML formulas [a]⟨b⟩T and ⟨a⟩([b]⟨c⟩T) but does not satisfy [a]⟨b⟩⟨c⟩T.

## Homework 11, Tuesday 24-10-2023

(Due: 31-10-2023 at 10am; accepted without penalty until 1-11-2023 at 10am)
1. Consider the HML formula φ = [a]([b]⟨c⟩T $\wedge$ ⟨b⟩[a]F).
Give an example process $P$ that satisfies the formula φ.
Give an example process $Q$ that does not satisfy the formula φ.
Also, give another HML formula without using the negation symbol, that holds for all processes for which φ does not hold.
2. Show that (infinitary, strong) completed trace equivalence is incomparable with (strong) simulation equivalence. This means that neither of them is finer-or-equal than the other.
3. Let X be the process given by the recursive equation X = a.(b.X + c.X)
and Y be the process given by the recursive equation Y = a.b.Y + a.c.Y.
1. Draw the process graph representations of X and Y.
2. Draw the process graph of the CSP process X ||S Y where S is the set {a,b,c}.
3. Draw the process graph of Y ||S Y.
4. Use the structural operational semantics of CSP to derive one of the transitions of X ||S Y.
4. Given a preorder $\sqsubseteq$ on a set $X$, let $\equiv$ be the kernel of $\sqsubseteq$, and let $\leq$ be the relation on the equivalence classes of $\equiv$ defined by $[x]_\equiv \leq [y]_\equiv$ iff $x \sqsubseteq y$. Here $[x]_\equiv$ denotes the $\equiv$-equivalence class of $x\in X$.
1. Show that $\leq$ is well-defined, in the sense that whether $A \leq B$ holds, for $\equiv$-equivalence classes $A$ and $B$, is independent of the choice of representatives $x\in A$ and $y \in B$ of these equivalence classes, when applying the above definition.
2. Show that $\leq$ is a partial order.

## Homework 12, Thursday 26-10-2023

(Also due: 31-10-2023 at 10am; accepted without penalty until 2-11-2023 at 10am)
1. Give a simple algorithm A that transforms process graphs G into A(G), such that A(G) and A(H) are rooted branching bisimulation equivalent if and only if G and H are branching bisimulation equivalent.
2. Question 1 from last week, but now for Counterexamples 1, 8, 9, 14 and 15.
3. Sequencing is a binary operation defined on any process graphs; it starts with its second component as soon as its first component cannot do any further actions.
Sequential composition, on the other hand, is defined on process graphs equipped with a state-labelling, where some states are marked with the symbol for successful termination, ✔. Here the second component starts only when the first one successfully terminates. This is the operator that occurs in ACP.

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.

1. Is sequential composition (as used e.g. in ACP) compositional for partial trace equivalence? Give a counterexample, or show why.
2. Is sequential composition compositional for completed trace equivalence? Give a counterexample, or show why.
3. Is sequencing compositional for partial trace equivalence? Give a counterexample, or show why.
4. Is sequencing compositional for (strong) completed trace equivalence? Give a counterexample, or show why.
5. Is partial trace equivalence a congruence for sequencing? Show why your answer is correct.
6. Is (strong) completed trace equivalence a congruence for sequencing? Show why your answer is correct.

## Homework 13, Tuesday 31-10-2023

(Due: 7-11-2023 at 10am; accepted without penalty until 8-11-2023 at 10am)
1. Model as an LTL formula:
1. If at any time the condition φ is satisfied then from that point onwards we will surely reach a state where ψ holds.
2. If the condition φ is satisfied infinitely often then we will surely reach a state where ψ holds.
2. For each of the following LTL formulae, show a state in a Kripke structure for which this formula holds, and show a state in a Kripke structure for which it doesn't hold.
1. $\textbf{G}(\textbf{F}p \wedge \textbf{F}\neg p)$.
2. $(p \textbf{U} (q \textbf{U} r))$.
3. $\textbf{F}(\textbf{G}p \rightarrow (q \textbf{U} r))$.
3. Which of the following formulae hold in the initial state of the Kripke structure depicted on the right?
1. $\textbf{G}(p \vee q)$
2. $\textbf{F}\textbf{G}(p \vee q)$
3. $\textbf{F}(\textbf{G}p \vee \textbf{G}q)$
4. $\textbf{G}(q \rightarrow (q \textbf{U}p))$
5. $\textbf{G}((p \wedge \neg q) \rightarrow \textbf{X}q$
6. $\textbf{G}((p \wedge q) \rightarrow \textbf{X}(q \textbf{U}p))$
4. This question is about mutual exclusion algorithms for two processes. Such an 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 finite 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 processes A and B are never simultaneously in their critical section, and to guarantee that both processes keep making progress. It is correct if these requirements are met.

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.

1. Formulate an LTL property in terms of these four atomic propositions (or others if needed) expressing the correctness of the algorithm.
2. (harder) Formulate an LTL property saying that if Process $A$ intends to go critical, then Process $B$ will enter its critical section at most once before $A$ does.
As requested during the tutorial, here is my answer to the last question: $\textbf{G}\left( \textit{IntentA} \rightarrow \textit{CritB} \mathrel{\textbf{U}}\rule{0pt}{13pt} \left(\neg \textit{CritB} \mathrel{\textbf{U}} \big(\textit{CritB} \mathrel{\textbf{U}}\rule{0pt}{10pt} (\neg \textit{CritB} \mathrel{\textbf{U}} \textit{CritA})\big)\right)\right)$ Here $\textbf{G}(\textit{IntentA} \rightarrow \psi)$ is a formula that says "whenever Process A intends to go critical, the condition $\psi$ holds". The task is thus to formulate a $\psi$ that says (i) that Process A will enter its critical section, and (ii) before that happens Process B will enter its critical section at most once. Note that B entering the critical section is a transition from a state where $\neg \textit{CritB}$ holds to one where $\textit{CritB}$ holds. Thus, between the assumed state where $\textit{IntentA}$ holds until the promised state where $\textit{CritA}$ holds, there can be at most 4 intervals: first a sequence of states where $\textit{CritB}$ holds, then a sequence of states where $\neg\textit{CritB}$ holds, then a sequence of states where $\textit{CritB}$ holds, and finally a sequence of states where $\neg\textit{CritB}$ holds. This alternation is provided by taking $\psi := \textit{CritB} \mathrel{\textbf{U}}\rule{0pt}{13pt} \left(\neg \textit{CritB} \mathrel{\textbf{U}} \big(\textit{CritB} \mathrel{\textbf{U}}\rule{0pt}{10pt} (\neg \textit{CritB} \mathrel{\textbf{U}} \textit{CritA})\big)\right)$. Naturally, it could occur that any or all these intervals are empty; this is allowed by the until-operators in $\psi$.

## Portfolio composition, Thursday 2-11-2023

Today you are invited to select which of your homeworks 1-10 you want to include in your mid-session portfolio. This portfolio determines 30% of your final grade. There also will be a 30% end-session portfolio, and a 40% final exam (in May) (with a must-pass hurdle). The portfolio interface will stay open 1 week.

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.

## Homework 14, Thursday 2-11-2023

(Also due: 7-11-2023 at 10am; accepted without penalty until 8-11-2023 at 10am)
1. Consider the CTL formulas AF EGp and AG EFp. Give examples of Kripke structures in which one holds and not the other, and vice versa. (Partial credit for showing Kripke structures illustrating the difference between the four formulas AFp, EFp, EGp and AGp.)
2. As mentioned in class, the LTL formula FGa cannot be accurately translated into CTL. Four candidate CTL translations are obtained by writing AF or EF for F, and likewise of G. Show that none of these translations are accurate, by exhibiting a state in a Kripke structure on which they give different results.
3. Which of the following CTL formulae hold in the initial state of the Kripke structure depicted above (for HW13 Q3)?
1. $\textbf{AF}(p \wedge q)$
2. $\textbf{AF}\textbf{AG}(p \vee q)$
3. $\textbf{AF}(\textbf{EG}p \wedge \textbf{EG}q)$
4. $\textbf{AG}(q \rightarrow \textbf{A}(q \textbf{U}p))$
5. $\textbf{A}(\textbf{E}(\neg q\textbf{U}p)\textbf{U}q)$
6. $\textbf{AG}((p \wedge q) \rightarrow \textbf{AX E}(q \textbf{U}p))$

## Mid session feedback form, Friday 3-11-2023

Here is a feedback form on this course. We would appreciate it if you would fill it in. The identity of submitters is not recorded.

## Homework 15, Tuesday 7-11-2023

(Due: 14-11-2023 at 10am; accepted without penalty until 15-11-2023 at 10am)
1. Give an LTL formula that show the difference between the processes of counterexamples 2, 5 and 12 (cf. HW10).
2. Give a CTL formula that show the difference between the processes of counterexamples 8, 5 and 12 (cf. HW10) [, or show that there isn't any -- this remark can be added to each question I ask].
1. Give a CTL-X formula that shows the difference between the processes d+τ.(ac+b) and d+ac+τ.(ac+b).
2. Give a CTL-X formula that shows the difference between the processes b+τ.(a+b) and b+a+τ.(a+b).
3. The dual of a logical operator $O(\phi,\psi)$ is $\neg O(\neg \phi, \neg \psi)$. Note that the dual of the dual of $O(\phi,\psi)$ is (logically equivalent to) $O(\phi,\psi)$ itself. The dual of $\phi \wedge \psi$ is (logically equivalent to) $\phi \vee \psi$. Likewise, the dual of $\forall x.\phi$ in first-order predicate logic is $\exists x.\phi$ The dual of the LTL modality F is G. The dual of $\phi \textbf{U} \psi$ must be $\neg( (\neg \phi) \textbf{U} (\neg \psi))$. How can it be expressed without using negation?

## Homework 16, Thursday 9-11-2023

(Also due: 14-11-2023 at 10am; accepted without penalty until 15-11-2023 at 10am)
1. Use the partition refinement algorithm on the states of a.(a(a+aa)+aa)+aaa. Show the steps. With how many bisimulation equivalence classes do you end up?

## Homework 17, Tuesday 14-11-2023

(Due: 21-11-2023 at 10am; accepted without penalty until 22-11-2023 at 10am)
1. Use the partition refinement algorithm for branching bisimilarity on the states of τ.(τ.(a+τ)+τ.a)+τ.(τ(a+τ)+a). Show the steps. Provide a branching bisimilar process graph with as few states as possible.
2. Provide an efficient algorithm for deciding rooted branching bisimilarity of process graphs. You may use the partition refinement algorithm for branching bisimilarity as a subroutine, without explaining it further.
3. Sequencing is a binary operation defined on process graphs without termination predicates; it starts with its second component as soon as its first component cannot do any further actions.
Give a correct structural operational semantics in GSOS format of the sequencing operator. (A wrong definition already occurred in HW9 Q3.)

## Homework 18, Thursday 16-11-2023

(Also due: 21-11-2023 at 10am; accepted without penalty until 22-11-2023 at 10am)
1. Translate the ACP implementation of the alternating bit protocol that you can find in the book of Fokkink into CCS and into CSP. Would you have to adapt the specifications well (and how)?
2. Exercise 6.1.2 in Fokkink.
3. Let's simplify the alternating bit protocol by omitting the alternating bit. Instead, the receiver send back the signal "success" or "failure" depending on whether it received a correct or a corrupted message. The sender simply resends the last message if it receives a "failure" or the corrupted acknowledgement $\bot$; upon receiving a "success" it proceeds with the next message. Does this version of the protocol work correctly? Explain your answer.

## Homework 19, Tuesday 21-11-2023

(Due: 29-11-2023 at 10am; accepted without penalty until 30-11-2023 at 10am)

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}$

## Homework 20, Thursday 23-11-2023

(Also due: 29-11-2023 at 10am; accepted without penalty until 30-11-2023 at 10am)
1. Give a Petri net for the following CCS expressions (with $\textbf{0}$ elided):
1. $a.(b + c.\bar{d})$
2. $\big(a.(b + c.\bar{d}) | \bar{b}.d\big)\backslash d$
3. $a+X$ where $X$ is given by the recursive equation $X=d.X$.
2. Let's define a step-trace of a Petri net to be sequence, not of actions, but of multisets of actions, such that the represented system can perform the sequence in succession, at each step performing the required multiset of actions simultaneously. For example, the process $a.(b + (c|d))$ would have the following completed step-traces:

{$ab, acd, adc, a[cd]$}

Here $[cd]$ denotes the multiset containing c and d one time each.
1. Give the set of completed step traces of $a.(b + c) | d$.
2. Give an example of two processes that are strong bisimulation equivalent but have different step-traces.
3. Give an example of two processes that have the same partial step traces, but different partial-order traces.
3. Consider a process with the following set of completed step traces: $\{bad,[ab]d,abd,a[bd],adb,acd,a[cd],adc\}$. Thus, in each run, the actions a, d and one out of c or b occur once each, subject to the following restrictions:
• b and c can never occur in the same trace.
• if c happens, it must be after a, and
• a happens before d.
Moreover, the choice between b and c should be made only after execution of a.
Moreover, the choice between $b$ and $c$ should be as late at possible, so that if either $b$ or $c$ is blocked by the environment, the other one is still possible.
1. Provide a Petri net with the above set of completed step traces and branching requirement.
2. What are the completed partial ordered traces of your net?
3. Give a CSP expression for this process that uses at most one occurrence of a choice operator (☐ or ⊓).
4. Give an ACP expression for this process that uses at most one +.
5. Give a CCS expression for this process that uses at most one +. You may have to smuggle in an internal action τ to make this possible.

 Rob van Glabbeek notes Rob.van.Glabbeek@ed.ac.uk