1. A binary relation ~ on a set D is an equivalence relation if it is
   • reflexive: p ~ p for all processes p in D,
   • symmetric: if p ~ q then q ~ p,
   • and transitive: if p ~ q and q ~ r then p ~ r.
   1. Give an example of an equivalence relation on the domain of all people.
   2. For each of these three requirements, give an example of a relation on people that is not an equivalence relation, because it fails this one requirement but satisfies the other two requirements.
   3. If ~ is an equivalence relation on D, and p is in D, then [p]_~ denotes the set of all processes in D that are equivalent to p. Such a set is called an equivalence class. Show (formally, by means of a mathematical proof) that the collection of all equivalence classes form a partitioning of D. This means that every p in D belongs to one and only one equivalence class.
   [None of this has been treated in class; (c) is a test of prior mathematical exposure to the notion of a mathematical proof. If this is hard, it is a good warm-up for bits of mathematical proof yet to come.]
2. Consider a vending machine that accept pieces of 20 cents, 50 cents and 1 dollar, and that can dispense (multiple) chocolate and pretzels, each of which costs 1 dollar. Draw an LTS whose transitions are labelled with "20c", "50c" or "$\$$1", indicating the reception by the machine of a coin inserted by a user, and by the actions "chocolate" or "pretzel", indicating the opening of the glass door of the machine behind which chocolate or pretzels are stored. (We abstract from the closing of the door after extraction of the pretzel, which happens automatically, and the appearance of a new pretzel behind the glass door afterwards.) Assume that the machine does not give change, and that it accepts any amount of surplus money. Try to make the number of states in your LTS as small as possible.
   Answer
3. Consider the process graph depicted in Counterexample 17, on page 49 of this paper. In that paper, the initial state is the unique one without incoming transitions. Formalise this graph in two ways:
   1. As a triple $(S,I,\rightarrow)$ of states, initial state and transition relation, as in the notes.
   2. As a tuple $(S,I,T,\textit{source},\textit{target},\ell)$, discussed in class.

1. Draw a process graph for the ACP expression a(bc+b(c+d)).
2. [Harder; can be skipped by students that merely aim for a basic good grade.]
   Give a formal definition of the sequential composition operator of ACP (see notes), in the style of the notes.
3. 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.
4. Give an example of a process that has no finite completed traces at all.
5. [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.

1. 1. Out of the following processes, which pairs are weak bisimulation equivalent?

      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

      Show the bisimulation or informally describe why there isn't any.
   2. Also tell which pairs are weak completed trace equivalent, and why or why not.
   3. And which pairs are strong completed trace equivalent, and why or why not.
   4. And which pairs are branching bisimulation equivalent, and why or why not.
2. Given an example of two processes of which some of the states may be marked with the termination predicate ✔, such that the two are (strong) bisimulation equivalent when discarding the termination predicate (without changing the states and transitions in any way), yet with the termination predicate taken into account they are completed trace equivalent but not bisimulation equivalent.
3. [Harder; can be skipped by students that merely aim for a basic good grade.]
   We write $Q \Longrightarrow Q$ if there are $Q_0$, $Q_1$, ... , $Q_n$ for some $n \geq 0$, such that $Q=Q_0$, $Q=Q_n$, and $Q_{i-1} \stackrel{\tau}\longrightarrow Q_i$ for all $i=1,...,n$.
   Here $Q$, $Q$ and the $Q_i$ are either processes or states in labelled transition systems. (In the next lecture we will drop the distinction between processes and states.) We write $P =_{BB} Q$ if there exists a branching bisimulation that relates the states $P$ and $Q$.
   1. Show that if $P =_{BB} Q$, $Q \Longrightarrow Q'$ and $P =_{BB} Q'$, then $P =_{BB} Q_i$ for any process $Q_i$ on the $\tau$-path from $Q$ to $Q'$.
   2. Does the same property also holds for weak bisimilarity $=_{WB}$? Give a proof or a counterexample.
   3. In class I defined a branching bisimulation $\mathcal{B}$ to satisfy the following transfer property:

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

      The handout, on the other hand, requires the following transfer property:

      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'$.

      Prove that these two definitions lead to the very same notion of branching bisimilarity.
      (As always, you may also answer the question by giving a counterexample showing that this is not the case.)

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).
   Answer
2. Express the behaviour of the gatekeeper from Homework 3.2 by a system of recursive equations.
   Answer
3. Describe the relay race in CCS in a similar way as the class notes describe it in ACP.
   Answer

1. For which possible choices of Q and R are there transitions of the form a.(c+b) | ((c+a) | b) --τ--> Q --τ--> R in the labelled transition system of CCS? (In CCS expressions action prefixing binds strongest of all operators. Moreover, I leave out trailing 0s, so c+b means c.0+b.0 .) Give a proof tree of the formal derivation of one of those transitions from the structural operational rules of CCS.
   Answer
2. [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.
3. [Hard; can be skipped by students that merely aim for a basic good grade.]
   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 ~.
   Answer: We need to show three things:
   1. ~_L is a congruence
   2. ~_L is finer than (or equal to) ~
   3. Any other congruence that is finer than ~ is also finer than (or equal to) ~_L.

   Ad i: We need to show that if P ~_L Q and $D[\ ]$ is a context, then D[P] ~_L D[Q]. So suppose P ~_L Q. This means that for any L-context C[ ] we have C[P] ~ C[Q]. What we have to show is that for any L-context C[ ] we have C[D[P]] ~ C[D[Q]], because that's the definition of D[P] ~_L Q[D]. But this holds, because a context $C[D[\ ]]$ is just a context $E[\ ]$.

   Ad ii: Suppose P ~_L Q. This means that for any L-context C[ ] we have C[P] ~ C[Q]. This holds in particular for the trivial context, consisting of one single hole. If T[ ] is the trivial context, then T[P] = P. Thus P ~_L Q implies P ~ Q, which was to be shown.

   Ad iii: Let $\approx$ be any other congruence that is finer then ~. Suppose $P \approx Q$. Then, for any context $C[\ ]$ we have $C[P] \approx C[Q]$, using that $\approx$ is a congruence, and thus $C[P] \sim C[Q]$, using that $\approx$ is finer than $\sim$. By definition this means that $P \sim_L Q$, which had to be shown.

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)?
   Answer
2. Formally derive the axiom (B) for branching bisimilarity (see notes) from the axioms for weak bisimilarity for CCS.
   Answer

1. Give a CCS expression for the vending machine intended by Q2 of HW1. This involves declaring a recursive specification.
   Answer: \[\begin{array}{lcl} X_0 &=& 20.X_{20} + 50.X_{50} + 100.X_{100} \\ X_{20} &=& 20.X_{40} + 50.X_{60/70} + 100.X_{100} \\ X_{40} &=& 20.X_{60/70} + 50.X_{80/90} + 100.X_{100} \\ X_{50} &=& 20.X_{60/70} + 50.X_{100} + 100.X_{100} \\ X_{60/70} &=& 20.X_{80/90} + 50.X_{100} + 100.X_{100} \\ X_{80/90} &=& 20.X_{100} + 50.X_{100} + 100.X_{100} \\ X_{100} &=& 20.X_{100} + 50.X_{100} + 100.X_{100} + \textit{pretzel}.X_0 + \textit{chocolate}.X_0\\ \end{array}\]
2. Recall the specification and implementation of the relay race in CCS (HW 6, Q3):
   Specification:    start.finish.0

   Implementation:    (R₁ | R₂)\$\{$handover$\}$    where
   R₁ = start.handover.0
   R₂ = 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.
3. Let the processes $X$, $Y$, $Z$ and $W$ be defined by the equations \[\begin{array}{lcl} X &=& b.Y + c.X \\ Y &=& d.(e.X+b.Y) \\ Z &=& b.d.W + c.(b.d.W + c.Z) \\ W &=& e.Z + b.d.W \end{array}\] Proof that $X=Z$, using the CCS axiomatisation of strong bisimilarity with RDP and RSP.
   Answer: Consider the recursive specification $\mathcal{S}$ given by \[\begin{array}{lcl} U &=& b.V + c.(b.V + c.U) \\ V &=& d.(e.U + b.V) \end{array}\] Clearly, $\mathcal{S}$ is guarded. Filling in $(Z,d.W)$ for $(U,V)$ yields two true equations, as followed directly from the equations for $Z$ and $W$. Hence $(Z,d.W)$ is a solution of $\mathcal{S}$. Likewise, filling in $(X,Y)$ for $(U,V)$ yields two true equations. Here we apply RDP to replace the $X$ in the body of the defining equation for $X$ by that body itself. So $(X,Y)$ is also a solution of $\mathcal{S}$. By RSP, two solutions of the same guarded recursive specification must be equal, so it follows that $X=Z$ (and $Y=d.W$).

1. Model the relay race in CSP.
   Answer
2. How would you translate the CSP expressions (a ☐ b) ⊓ c and (a ⊓ b) ☐ c into CCS? Here I omitted trailing .0's.
   Answer
3. 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?
   Answer: This recursive specification is guarded, because each call to $Y$ sits in the scope of an action-prefixing operator ($a.$, $d.$ and $e.$). Therefore, by RDP and RSP, it has a unique solution up to strong bisimilarity. The presence of the parallel and restriction operators plays no role.
4. In a proposed extension of CSP there is a "sliding choice" operator $\triangleright$, which treats its left argument as an external choice, and its right argument as an internal one. Its operational rules are \[ \frac{P \stackrel{a}{\rightarrow} P'}{P \triangleright Q \stackrel{a}{\rightarrow} P'}~(a \neq \tau) \qquad \frac{P \stackrel{\tau}{\rightarrow} P'}{P \triangleright Q \stackrel{\tau}{\rightarrow} P'\triangleright Q} \qquad \frac{}{P \triangleright Q \stackrel{\tau}{\rightarrow} Q} \] Is this operator compositional for strong bisimilarity? How do you know this?
   Answer: Yes, because the above rules are on GSOS format.
5. Here is an attempted operational semantics of the sequencing operator:

   P --a--> P' ------------------------ (for P' $\neq$ 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).
   Answer: No, it is not in GSOS format. The second rule fails this format because the right-hand side of its premise features a constant. (The first rule also fails this format, because it has a side-condition that cannot be expanded away.)
   To show that strong bisimulation is not a congruence, consider the processes $P=a.0$, $Q=a.(0+0)$ and $R=b.0$. Now $P$ and $Q$ are strongly bisimilar, but $P;R$ and $Q:R$ are not. In fact $P;R$ has a trace $ab$, whereas $Q;R$ can never do a $b$. Here it is important that to match the second rule for ;, being equal to $0$ is taken literally; not up to bisimilarity or so.

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

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.
   Answer
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.
   Answer
3. 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.
   Answer

1. Use the partition refinement algorithm on the states of a.(a.(a+a.a)+a.a)+a.a.a. Trailing .0's are elided. Show the steps. With how many bisimulation equivalence classes do you end up?
   Answer
2. 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.
   Answer
3. 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.
   Answer: First run the partition refinement algorithm for branching bisimilarity, terminating with exactly one block $B_e$ for each branching bisimilarity equivalence class of states $e$. Next, consider all strong potentials $(a,B_e)$ for that partition; they hold for a state $s$ iff $s$ can do an $a$-transition to a state in block $B_e$. Finally, consider two states rooted branching bisimilar iff they have the same potentials as defined above. (Thus, this algorithm does all the rounds for BB and then one round as for strong bisimilarity.)

1. Modify the definition of weak completed trace semantics (or invent new semantic equivalences from scratch) in six different ways, namely such that
   1. deadlock = livelock and escapable divergence = normal progress,
   2. escapable divergence = normal progress, and livelock differs from deadlock and from normal progress,
   3. deadlock = livelock and escapable divergence differs from livelock and from normal progress,
   4. livelock = escapable divergence, different from deadlock and progress,
   5. deadlock = livelock = escapable divergence, different from progress,
   6. all four phenomena are distinguished.
   In all cases deadlock should be distinguished from normal progress. Your notions of weak completed trace equivalence should all be strictly finer than finitary weak partial trace equivalence, as defined in the class notes, and strictly coarser than strong bisimilarity. Also, the definitions should be such that upon restricting attention to processes without divergence, the resulting equivalences coincide with (finitary or) infinitary weak completed trace equivalence as in the notes. They should also be congruences for abstraction (τ_I); no need to prove this. Finally, they should make sense from the perspective of comparing general processes (not just these examples).
   Answer

1. 1. Formulate a safety property that is satisfied by $a.b+a.c$, but not by $c.a+b.a$.
   2. Formulate a safety property that is satisfied by $a.b+a.c$, but not by $a.(b+c)$.
   Answer
2. 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 specification as well (and how)?
   Answer
3. Exercise 6.1.2 in Fokkink.
   Answer
4. 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.
   Answer

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.)
   Answer
2. Which of the following CTL formulae hold in the initial state of the Kripke structure depicted on the right?
   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))$
   Answer

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.
      Answer: $\textbf{G}(\varphi \Rightarrow \textbf{F}\psi)$
   2. If the condition φ is satisfied infinitely often then we will surely reach a state where ψ holds.
      Answer: $\textbf{G}\textbf{F}\varphi \Rightarrow \textbf{F}\psi$
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))$.
   Answer
3. 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.
   Answer
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.
      Answer: $\big(\textbf{G}\neg(\textbf{CritA} \wedge \textbf{CritB})\big) \wedge \textbf{G} \big(\textbf{IntentA} \Rightarrow \textbf{F}(\textbf{CritA})\big) \wedge \textbf{G} \big(\textbf{IntentB} \Rightarrow \textbf{F}(\textbf{CritB})\big)$
   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.
      Answer: \[\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$.

1. Which of the following LTL formulae hold in the initial state of the Kripke structure depicted above (for HW17 Q2)?
   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))$
   Answer
2. 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$.
   Answer
3. At https://doi.org/10.1016/S0304-3975(01)00300-0 you find a scientific paper. Translate the Petri net in Figure 1 in that paper to a process graph.
   Answer

For yet more fun, you can try the 2020 exam of this course. Questions 4(c)--(f) in that exam test material that has not been covered this year. Skipping those, you can get 88 points for this exam, and 84 of those constitute full credit (a mark of 100). The so-reduced exam is supposed to be done in 2.5 hours (unlike the 2023 and 2024 exams, which you have to do in 2 hours).

I propose that you try the exams first before getting confronted with the answers. Let's do a session about 2 weeks before the final exam (and we know when that is only in March) in which I (or one of you) solve(s) the 2020 exam questions on the whiteboard. I'll post the solutions to the 2023 exam here a week before that (or whenever you all want), and these can be discussed in that session as well. Let's use Piazza to make final plans (when the time comes).

And here is the exam and solutions of this year's exam.