Title: Reactive Systems

Q: An imperative program can also be represented as [...].
A: a function from one state to another

Front: How does one write the undefined part of a partial function \(⟦ U ⟧\)?
Back: \(⟦ U ⟧=\lambda s.\text{undefined}\)

Front: What is the fundamental program for a reactive system?

Front: What is the intuition behind process algebras?
Back: If we combine two parallel processes \(P\) and \(Q\), the result is again a process, whose behaviour depends on that of \(P\) and \(Q\) and the method we used to compose them.

Front: What is the basic mode of interaction between processes?
Back: Synchronized communication; every synchronized communication can be made asynchronous, but not the other way around.

Front: What does the abbreviation CCS stand for in the context of reactive systems?
Back: Calculus of Communicating Systems

Front: In CCS, what components does a process have?
Back: • A name
• An interface consisting of a collection of communication ports or channels

Front: By which notation are input/output ports distinguished in CCS?
Back: • \(a\) for the input, and
• \(\overline{a}\) for the output on port \(a\)

Front: What does \(\mathbf{0}\) stand for in CCS?
Back: The process that performs no action whatsoever.

Front: State the formal rule for action prefixing.
Back: If \(P\) is a process and \(a\) is a label then \(a.P\) is also a process.

Front: What is a label?
Back: It is an input or output action on a communication port for a given process.

Front: How does one define an everlasting clock in CCS?
Back: \(\text{Clock} \overset{\text{def}}{=}\overline{\text{tick}}.\text{Clock}\)

Front: What does the \(+\) operator mean in CCS?
Back: It signifies choice: in \(P + Q\), choosing to perform initially an action from \(P\) will pre-empt the execution of actions from \(Q\) and vice versa.

Front: State the formation rule for choice.
Back: If \(P\) and \(Q\) are processes then so is \(P+Q\).

Front: What does the expression \(P|Q\) stand for?
Back: Two processes \(P\) and \(Q\), running independently, and able to communicate via complementary ports.

Front: What is the restriction operator in CCS?
Back: The restriction operator specifies that some ports \(L\) can only be used for communication within a process \(P\).
We write this as \(P\backslash L\).
For example, when we write
\((\text{Albert}|\text{Linchuan})\backslash \text{Ice-cream }|\text{Tami}\)
that means that Albert and Linchuan have access to icecream, while Tami is excluded from it.

Front: In CCS, what is label renaming and how does one write it?
Back: If \(P\) is a process and \(f\) is a function from labels to labels, then \(P[f]\) is a process.
For example, if we have a general vending machine \(\text{VM}\overset{\text{def}}{=}\text{coin}.\overline{\text{item}}.\text{VM}\), then \(\text{CHM}\overset{\text{def}}{=}\text{VM}[\text{choc}/\text{item}]\) is a chocolate machine.

Front: When we want to write that a process \(\text{CS}\) evolved into another process \(\text{CS}_1\) due to the action \(\overline{\text{pub}} \), how do we do that?
Back: \(\text{CS} \overset{\overline{\text{pub}}}{\rightarrow} \text{CS}_1\)
This is generalizable to arbitrary state machines:

Front: What is the issue with writing down the formula for two parallel communicating processes \(P_1, P_2\) and \(Q_1, Q_2\), and how is it solved?
Back: If one process transitions via \(\text{a}\) and the other via \(\overline{\text{a}}\), then we don't know what to write in the transition diagram.
The solution is to use a new label \(τ\) for the state transition:
\((P_1|Q_1) \backslash \{a\} \overset{τ}{\rightarrow} (P_2|Q_2) \backslash \{a\}\)
These actions \(τ\) are unobservable.

Front: In a labelled transition system, when is a state \(p'\) reachable from a process \(p\)?
Back: Iff there exists a directed path from \(p\) to \(p'\).

Front: Give the definition for a labelled transition system (LTS).
Back: A triple \((\textbf{Proc}, \textbf{Act}, \{\overset{α}{\rightarrow}|α \in \textbf{Act}\})\), where
• \(\text{Proc}\) is a set of states or processes
• \(\text{Act}\) is a set of actions or labels
• \(\{\overset{α}{\rightarrow}|α \in \text{Act}\}: \text{Proc} \times \text{Proc}\) is a transition relation, for every \(α \in \text{Act}\).

Front: What does the notation \(s \overset{α}{\nrightarrow}\) mean?
Back: There is no \(s'\) so that \(s \overset{α}{\rightarrow} s'\).

Q: The state transition relation is transitive by [...]
A: concatenation of the strings of the action, e.g. \(s \overset{αw}{\rightarrow} s'\) iff there is a state \(t\) such that \(s \overset{α}{\rightarrow} t\) and \(t \overset{w}{\rightarrow} s'\).

Front: What does \(s \rightarrow^* s'\) mean?
Back: \(\rightarrow^*\) is the reflexive and transitive closure of the relation \(\rightarrow\).
\(s \rightarrow^* s'\) iff \(s \overset{w}{\rightarrow} s'\) for some \(w \in \textbf{Act*}\).

Q: \(\textbf{Act}*\) is [...]
A: the set of all actions and the empty action \(ε\).

Front: What is the order of operators in CCS?
Back: From tightest to loosest:
• \ and []
• .
• |
• +

Front: How is action prefixing defined in SOS?
Back: If a process is prefixed by \(α\), it can transition via \(α\).

Q: SOS stands for [...]
A: structural operational semantics.

Q: LTS stands for [...]
A: labelled transition system.

Front: How is process choice defined in SOS?
Back: If \(P_j\) transition to \(P_j'\) via \(α\), then the choice between \(P_j\) and other processes can also transition to \(P_j'\) via \(α\).

Front: How is parallel process communication defined in SOS?
Back: If \(P\) and \(Q\) are running in parallel, then \(P\) can still transition to \(P'\) (and the other way around).
Also, two mutually blocking processes can transition via \(τ\).

Front: How is process restriction defined in SOS?
Back: \(P\) can transition to \(P'\) via \(α\) if \(L\) is restricted only if \(α\) and \(\overline{α}\) are not in \(L\).

Front: How is variable renaming defined in SOS?
Back: If you can transition via \(α\), then after renaming with \(f\) you transition via \(f(α)\).

Front: How is process definition formalized in SOS?
Back: If \(K \overset{\text{def}}{=} P\), then \(K\) behaves as \(P\) in transitions.

Front: When is a relation \(R\) an equivalence releation?
Back: If it is
• reflexive
• symmetric
• transitive

Front: When is a relation a preorder?
Back: If it is
• reflexive and
• transitive

Front: What does \(\text{Spec }R\text{ Imp}\) mean?
Back: If we have an equivalence relation \(R\), we want our specification \(\text{Spec}\) to be equivalent to our implementation \(\text{Imp}\) of the desired process.

Front: What is congruence?
Back: Process descriptions that are related by \(R\) can be used interchangeably as parts of a larger process description.
More precisely, if \(P\text{ }R\text{ }Q\) and if \(C[]\) has a free substitution, then
\(C[P]\text{ }R\text{ }C[Q]\)

Front: What is the trace of a process \(P\)?
Back: A sequence \(α_1 \dots α_k \in \textbf{Act}^*\) of actions such that
\(P=P_0 \overset{α_1}{\rightarrow} P_1 \overset{α_2}{\rightarrow} \dots \overset{α_{k-1}}{\rightarrow} P_{k-1} \overset{α_{k}}{\rightarrow} P_{k}\).

Front: What is the completed trace of a process \(P\)?
Back: It's a trace that ends in a state from which no further transitions are possible.
More mathematically:
It's a sequence \(α_1, \dots α_k \in \textbf{Act}^*\) such that there exists a sequence of transitions
\(P=P_0 \overset{α_1}{\rightarrow} P_1 \overset{α_2}{\rightarrow} \dots \overset{α_{k-1}}{\rightarrow} P_{k-1} \overset{α_{k}}{\rightarrow} P_{k} \not \rightarrow\).

Front: When is a binary relation \(\mathcal{R}\) over the set of states of an LTS a bisimulation?
Back: Iff it equivalently relates two states to each other so that they can be transitioned to with the same actions.
More mathematically: Iff whenever \(s_1 \mathcal{R} s_2\) and \(α\) is an action:
If \(s_1 \overset{α}{\rightarrow} s_1'\) then there is a transition \(s_1 \overset{α}{\rightarrow} s_2'\) such that \(s_1' \mathcal{R} s_2'\);
If \(s_2 \overset{α}{\rightarrow} s_2'\) then there is a transition \(s_1 \overset{α}{\rightarrow} s_1'\) such that \(s_1' \mathcal{R} s_2'\);

Q: When two states \(s\) and \(s'\) are bisimilar, we write [...]
A: \(s \sim s'\).

Q: Two states are bisimilar iff [...]
A: there is a bisimulation that relates them.

Front: In which way is the relation \(\sim\) recursive?

Front: What is the definition of \(\sim\)?
Back: \(\sim\) is the set of all bisimulations.
\(\sim=\{\mathcal{R}|\mathcal{R} \text{ is a bisimulation}\}\)

Q: \(\prod_{i=1}^{k} P_i\) stands for [...]
A: \(P_1|P_2| \dots | P_k\).

Front: When is a binary relation \(\mathcal{R}\) over the states of an LTS a simulation?
Back: Iff whenever \(s_1 \mathcal{R} s_2\) and \(α\) is an action:
If \(s_1 \overset{α}{\rightarrow} s_1'\) then there exists a transition \(s_2 \overset{α}{\rightarrow} s_2'\) such that \(s_1' \mathcal{R} s_2'\).

Q: We say that \(s'\) simulates \(s\), written [...] iff there is [...]
A: \(s \underset{\sim}{\sqsubset} s'\); a simulation \(\mathcal{R}\) for which \(s \mathcal{R} s'\).

Q: Two states \(s\) and \(s'\) are [...], written [...], iff [...]
A: simulation equivalent; \(s \simeq s'\); \(s \underset{\sim}{\sqsubset} s'\) and \(s' \underset{\sim}{\sqsubset} s\) both hold.

Front: When is a binary relation \(\mathcal{R}\) a ready simulation?
Back: If it's a simulation and the states can transition further with the same action.
That is, whenever \(s_1 \mathcal{R} s_2\) and \(α\) is an action:
if \(s_2 \overset{α}{\rightarrow}\) then \(s_1 \overset{α}{\rightarrow}\).

Front: Which CCS operators preserve strong bisimilarity?
Back: All of them.

Q: For each action \(α\), we write [...] iff
either [...]
or [...].
A: \(P \overset{α}{\Rightarrow} Q\); \(α \not =τ\) and there are processes \(P'\) and \(Q'\) such that \(P (\overset{τ}{\rightarrow})^* P' \overset{α}{\rightarrow} Q' (\overset{τ}{\rightarrow})^* Q \); \(α=τ\) and \(P (\overset{τ}{\rightarrow})^* Q\)
Extra: We get from \(P\) to \(Q\) via a sequence of \(τ\)s with some \(α\) in the middle.

Front: When is a binary relation \(\mathcal{R}\) over a set of states a weak bisimulation?
Back: Iff for all \(s_1 \mathcal{R} s_2\) and actions \(α\) (including \(τ\)):
If \(s_1 \overset{α}{\rightarrow} s_1'\) then there exists a transition \(s_2 \overset{α}{\Rightarrow} s_2'\) such that \(s_1' \mathcal{R} s_2'\)
If \(s_2 \overset{α}{\rightarrow} s_2'\) then there exists a transition \(s_1 \overset{α}{\Rightarrow} s_1'\) such that \(s_1' \mathcal{R} s_2'\)

Q: Two states \(s\) and \(s'\) are [...], written [...], iff [...]
A: observationally equivalent (or weakly bisimilar); \(s \approx s'\); there is a weak bisimulation that relates them.

Front: To which CCS operators is \(\approx\) (observational equivalence) congruent?
Back: All except \(+\) (choice):

A strong bisimulation game has the following structure:
You start with an LTS \(L=(\textbf{Proc}, \textbf{Act}, \{\overset{α}{\rightarrow}|α \in \textbf{Act}\})\) and a configuration \((s_1, t_1)\).
There are also two players: an attacker and a defender.
Each round, the attacker can choose to perform a transition, either left (\(s \overset{α}{\rightarrow} s'\)) or right (\(t \overset{α}{\rightarrow} t'\)), with any action \(α\).
The defender then has to answer with an \(α\) transition, if the attacker has chosen left, the defender has to transition right, and left otherwise.

Q: In a strong bisimulation game, a play of the game is [...]
A sequence of actions is maximal if [...]
A: a maximal sequence of configurations formed by the players according to the rules, starting from the initial configuration \((s_1, t_1)\).; it can't be extended by either player while following the rules.

Front: In a strong bisimulation game, when does the attacker win?
Back: Iff the defender can't transition using the same action as the attacker

Front: In strong bisimulation games, when does the defender win?
Back: Iff:
• The attacker can't make any transition from the current state, or
• The play is infinite

Front: What is the relation between winning strategies in strong bisimulation games and strong bisimilarity?
Back: Two states \(s_1, t_1\) of an LTS are strongly bisimilar iff the defender has a universal winning strategy.
(They aren't strongly bisimilar iff the attacker has a universal winning strategy).

Front: When I talk of a weak bisimulation game, you know what is being talked about, right?
Back: Yeah. It's a bisimulation game, just with the defender being able to also answer with a weak transition relation \(\overset{α}{\Rightarrow}\) to the action \(\overset{α}{\rightarrow}\).
The attacker can only use full transitions \(\overset{α}{\rightarrow}\).

Front: When is an LTS called regular?
Back: If it has a finite set of states and finitely many transitions.

Front: What is saturation?
Back: The process of turning a pair of LTSs from a version with weak bisimilarity to a version with strong bisimilarity.

Front: What is a poset?
Back: A poset is a pair \((D, \sqsubseteq)\), where \(D\) is a set and \(\sqsubseteq\) is a binary relation over \(D\) so that \(\sqsubseteq\) is
• reflexive
• antisymmetric
• transitive

Front: How are the least upper bound (lub) and greatest lower bound (glb) defined?
Back: An element \(d\) of a poset \((D, \sqsubseteq)\) is the least upper bound/greatest lower bound of a set \(X \subseteq D\) iff
• \(d\) is an upper/lower bound for \(X\) and
• \(d \sqsubseteq d'\) for every \(d' \in D\) that is an upper/lower bound for \(X\).

Q: [...] signifies [...]
A: \(\bigsqcap X / \bigsqcup X\); the greatest lower bound/least upper bound of \(X\).

Front: When is a poset \((D, \sqsubseteq)\) a complete lattice?
Back: Iff \(\bigsqcap X\) and \(\bigsqcup X\) exist for every subset \(X\) of \(D\).

Q: Let \((D, \sqsubseteq)\) be a poset. A function \(f: D \mapsto D\) is monotonic iff [...]
A: \(d \sqsubseteq d'\) implies that \(f(d) \sqsubseteq f(d')\) for all \(d, d' \in D\).

Front: State Tarski's fixed point theorem.
Back: Let \((D, \sqsubseteq)\) be a complete lattice, and let \(f: D \mapsto D\) be monotonic.
Then \(f\) has a largest fixed point \(z_{\text{max}}\) and a least fixed point \(z_{\text{min}}\) given by
• \(z_{\text{max}}=\bigsqcup \{x \in D | x \sqsubseteq f(x)\}\),
• \(z_{\text{min}}=\bigsqcap \{x \in D | f(x) \sqsubseteq x\}\)

Front: How does one compute the smallest/greatest fixed point for a function on a finite complete lattice?
Back: By recursively applying the function to \(\bot / \top\).
More formally, let \(f^{n+1}(d)=f(f^n(d))\), and \(f^0(d)=d\). Then there must be some \(m \in ℕ\) so that \(z_{\text{min}}=f^m(\bot)\), and there must be some \(M \in ℕ\) so that \(z_{\text{min}}=f^M(\top)\). These can be found by iteratively applying \(f(d)\).

Front: How can Tarski's fixed point theorem be applied to bisimulation, and what is its relation to the strongest bisimulation \(\sim\)?
Back: The relation \(\sim\) is the largest fixed point for the function mapping pairs of states to their bisimulation.
Given an LTS, \((2^{(\textbf{Proc} \times \textbf{Proc})}, \subseteq)\) is a complete lattice.
Then the strongest bisimulation is an element of that complete lattice, and can be found as follows:
Let \(\mathcal{F}(\mathcal{R})\) be a function that maps from \(p, q \in \textbf{Proc}\) to all possible bisimulated states of \(p,q\) (that is, all actions a defender could play in the bisimulation game as response to \(p,q\)).
Then it is the case that
\(\sim =\bigsqcup \{\mathcal{R} \in 2^{(\textbf{Proc} \times \textbf{Proc})} | \mathcal{R} \subseteq \mathcal{F}(\mathcal{R})\}\)

Front: How can one compute \(\sim\) for a given finite LTS?
Back: Use the function \(\mathcal{F}\), defined as follows:
The compute the non-increasing sequence
until it reaches a fixpoint.

Front: In value-passing CCS, what is the rule for input prefixing?

Front: In value-passing CCS, what is the rule for output prefixing?

Front: In value-passing CCS, how is replacement with expressions defined?
Back: where \(\mathbf{A}\) is a parameterized constant that refers to a process.

Front: When is a variable \(y\) in CCS with value passing bound?
Back: Iff it occurs within the scope of an input prefix of the form \(a(y)\) or of a parameterized constant \(A(x_1, \dots, y, \dots, x_n)\).

Front: What are the rules for introducing if-then clauses in value-passing CCS?

Front: Give the syntax that describes all sentences of Hennessy-Milner logic.
Back: \(F, G::=\textit{t}\!\textit{t} | \textit{f}\!\textit{f} | F \land G | F \lor G | \langle a \rangle F | [a] F\)

Front: In the grammar \(F, G::=\textit{t}\!\textit{t} | \textit{f}\!\textit{f} | F \land G | F \lor G | \langle a \rangle F | [a] F\), what do the individual components stand for?
Back: \(\textit{t}\!\textit{t}\) and \(\textit{f}\!\textit{f} \) stand for 'true' and 'false', respectively, and \(a \in \textbf{Act}\).

Q: The abbreviation [...] stands for [...].
A: HML; Hennessy-Milner Logic

Q: In HML, a process [...] iff it [...].
A: satisfies \(\langle a \rangle F\) for some \(a \in \textbf{Act}\); affords an \(a\)-labelled transition leading to a state satisfying \(F\)

Q: In HML, a process [...] iff [...].
A: satisfies \([a] F\) for some \(a \in \textbf{Act}\); all its \(a\)-labelled transition leads to a state satisfying \(F\)

Front: In HML, what does \(⟦F⟧\) stand for?
Back: The set of all processes that satisfy \(F\).

Q: In denotational semantics, \(⟦\textit{t}\!\textit{t}⟧=\) [...].
A: \(\text{Proc}\)

Q: In denotational semantics, \(⟦\textit{f}\!\textit{f}⟧=\) [...].
A: \(\emptyset\)

In HML, \(⟦\langle a \rangle F⟧\) is equal to \(\langle \cdot a \cdot \rangle ⟦F⟧\), where \(\langle \cdot a \cdot \rangle S\) is defined as the set of processes that can transition to an element in \(S\) via \(a\), mathematically \(\langle \cdot a \cdot \rangle S\)\(=\)\(\{p \in \text{Proc} | p \overset{a}{\rightarrow} p' \text{ and } p' \in S \text{ for some } p'\}\).

In HML, \(⟦[a] F⟧\) is equal to \([ \cdot a \cdot ] ⟦F⟧\), where \([ \cdot a \cdot ]S\) is defined as the set of processes that become an element in \(S\), no matter how they perform an \(a\)-transition. Mathematically, \([ \cdot a \cdot ] S\)=\(\{p \in \text{Proc} | p \overset{a}{\rightarrow} p' \text{ and } p' \in S \text{ for each } p'\}\).

\(P \models \textit{t}\!\textit{t}\) for each \(P\)
\(P \models \textit{f}\!\textit{f}\) for no \(P\)
\(P \models F \land G\) iff \(P \models F\) and \(P \models G\)
\(P \models F \lor G\) iff \(P \models F\) or \(P \models G\)
\(P \models \langle a \rangle F\) iff \(P \overset{a}{\rightarrow} P'\) for some \(P'\) such that \(P' \models F\)
\(P \models [ a ] F\) iff \(P' \models F\) for all \(P'\) such that \(P \overset{a}{\rightarrow} P'\)

Let \(a^c\) stand for the negation of \(a\). Then the negations of all possible formulas can be constructed by
1. \(\textit{t}\!\textit{t}^c=\textit{f}\!\textit{f}\)
2. \(\textit{f}\!\textit{f}^c=\textit{t}\!\textit{t}\)
3. \((F \land G)^c=F^c \lor G^c\)
4. \((F \lor G)^c=F^c \land G^c\)
5. \((\langle a \rangle F)^c=[a]F^c\)
6. \(([ a ] F)^c=\langle a \rangle F^c\)

Q: A process \(P\) is [...] iff [...]
A: image finite; the collection \(\{P'|P \overset{a}{\rightarrow} P'\}\) is finite for each action \(a\).

Q: The [...] states that [...].
A: Hennessy-Milner theorem; two processes \(P, Q \in \textbf{Proc}\) are strongly bisimilar (\(P \sim Q\)) iff \(P\) and \(Q\) satisfy exactly the same formula in Hennessy-Milner logic

\(\text{Pos}(F)\) stands for \(F \lor \langle \textbf{Act} \rangle F \lor \langle \textbf{Act} \rangle \langle \textbf{Act} \rangle F \dots = \bigvee_{i \ge 0} \langle \textbf{Act} \rangle^i F\), recursively \(Y \overset{min}{=} F \lor \langle \textbf{Act}\rangle Y\). It means that \(F\) possibly holds at some point in the LTS.

\(\text{Inv}(F)\) stands for \(F \land [ \textbf{Act} ] F \land [ \textbf{Act} ] [ \textbf{Act} ] F \dots = \bigwedge_{i \ge 0} [ \textbf{Act} ]^i F\), recursively \(X \overset{max}{=} F \land [\textbf{Act}] X\). It means that every reachable state in an LTS has property \(F\).

Q: When we want the largest solution to a recursive HML formula \(X\), we write [...].
A: \(X \overset{\text{max} }{=} X\)

Q: When we want the smallest solution to a recursive HML formula \(X\), we write [...].
A: \(X \overset{\text{min} }{=} X\)

\(F \mathcal{U}^s G\), called strong until says that sooner or later the process \(p\) reaches a state where \(G\) is true and in all the states it traverses before \(F\) must hold. Recursively \(F \mathcal{U}^s G\) \(\overset{\text{min} }{=} G \lor (F \land \langle \textbf{Act} \rangle \textit{t}\!\textit{t} \land [\textbf{Act}]\)\((F \mathcal{U}^s G))\).

\(F \mathcal{U}^w G\), called weak until says that in the process \(p\) \(F\) must hold in all states \(p\) traverses until it reaches a state where \(G\) holds (although this might never happen). Recursively \(F \mathcal{U}^w G \overset{\text{max} }{=} G \lor (F \land [ \textbf{Act} ] (F \mathcal{U}^w G))\).

Q: The syntax of Hennessy-Milner logic with one variable \(X\), denoted [...] is given by the following grammar:

Semantically, a formula \(F\) is interpreted as [...]
A: \(\mathcal{M}_{\{X\} }\); a function \(\mathcal{O}_F: 2^{\textbf{Proc} } \mapsto 2^{\textbf{Proc} }\) that, given a set of processes that are assumed to satisfy \(X\), returns the set of processes that satisfy \(F\).

Front: In Recursive Hennesy-Milner logic with one variable \(X\), how is \(\mathcal{O}_F\) defined?
(Hint: it's very similar to Hennessy-Milner logic).

Front: In the context of recursive HML, how does one write the largest/least fixed point of \(\mathcal{O}_{F_X}\)?

Q: [...] stands for [...], recursively [...].
A: \(\text{Safe}(F)\); the set of processes that have a complete transition sequence \(p=p_0 \overset{a_1}{\rightarrow} p_1 \overset{a_2}{\rightarrow} p_2 \dots\) where each \(p_i\) satisfies \(F\); \(X \overset{\text{max} }{=} F \land ([\textbf{Act}] \textit{f}\!\textit{f} \lor \langle \textbf{Act} \rangle X)\)

Q: [...] stands for [...]. Recursively [...].
A: \(\text{Even}(F)\); the set of processes in which each of its complete transition sequences will contain at least one state that has the property \(F\); \(X \overset{\text{min} }{=} F \lor (\langle \textbf{Act} \rangle \textit{t}\!\textit{t} \land [ \textbf{Act} ] X)\)

In the game formulation of Hennesy-Milner logic, we have a formula \(F_X\) that may contain occurences of the variable \(X\), and an LTS \((\textbf{Proc}, \textbf{Act}, \{\overset{a}{\rightarrow}| a \in \textbf{Act}\})\).
The game takes place between two agents, an attacker and a defender.
The attacker is trying to prove that \(s \not \models F\), while the  defender is trying to prove that \(s \models F\).
The configurations of the game are pairs of the form \((s, F)\), where \(s \in \textbf{Proc}\) and \(F\) is a formula of Hennessy-Milner logic with one variable \(X\).

In the game formulation of HML with recursion, the successor function for a configuration \((s, F)\) is defined as follows:
• \((s, \textit{t}\!\textit{t})\) and \((s, \textit{f}\!\textit{f})\) have no successor configurations
• \((s, F_1 \land F_2)\) and \((s, F_1 \lor F_2)\) both have two successor configurations, namely \((s, F_1)\) and \((s, F_2)\)
• \((s, \langle a \rangle F)\) and \((s, [a] F)\) both have the successor configurations \((s', F)\) for every \(s'\) such that \(s \overset{a}{\rightarrow} s'\)
• \((s, X)\) has only one successor configuration \((s, F_X)\), where \(X\) is defined via either \(X \overset{\text{max} }{=}F_X\) or \(X  \overset{\text{min} }{=}F_X\)

Front: What are the rules for the game characterization of HML?
Back: The attacker picks a successor configuration for every current configuration of the form \((s, F_1 \land F_2)\) and \((s, [a] F)\)
The defender picks a successor configuration for every current configuration of the form \((s, F_1 \lor F_2)\) and \((s, \langle a \rangle F)\)

A game in recursive HML terminates if the state is \((s, \textit{t}\!\textit{t})\), in which case the defender wins or \((s, \textit{f}\!\textit{f})\), in which case the attacker wins, or the attacker gets stuck in the configuration \((s, [a]F)\) (the defender wins), or the defender gets stuck in \((s, \langle a \rangle F)\) (the attacker wins) when \(s \overset{a}{\not \rightarrow}\).
If the play is infinite, the attacker is the winner if \(X\overset{\text{min} }{=} F_X\), and the defender is the winner if \(X \overset{\text{max} }{=} F_X\).

Q: In general, a [...] has the form
[...], where
\(\mathcal{X}=\{X_1, \dots, X_n\}\) is a set of variables and, for \(1 \le i \le n\), the formula \(F_{X_i}\) is in \(\mathcal{M}_{\mathcal{X}}\) and can therefore contain any variable from \(\mathcal{X}\).
A: mutually recursive equational system; \(X_1=F_{X_1}\),
…,
\(X_n=F_{X_n}\)

Q: An equational system
is meant to describe [...]
A: a vector \((S_1, \dots, S_n)\) of sets of processes such that

Front: Why is the domain for mutually recursive equational systems \((2^{\textbf{Proc}})^n\)?
Back: For each formula, we need to consider all possible subsets of states the corresponding process can be in.
For \(n\) formulae, we then consider the cartesian product of all those possible subsets (because subsets of the states can be combined in any fashion).

Front: How is the partial order defined for states of mutually recursive equational systems, with states \(S_1, \dots S_n\).
Back: The partial order is defined component-wise:

Front: In mutually recursive equational systems, how are the greatest lower bound/the least upper bound defined, for a domain \((\mathcal{D}, \sqsubseteq)\)?
Back: Component-wise:

Front: In mutually recursive equational systems, what is a declaration?
Back: A declaration is a function \(D: \mathcal{X} \mapsto \mathcal{M}_{\mathcal{X}}\), associating a formula with each variable.
\(\mathcal{X}\) is the set of variables, and \(\mathcal{M}_{\mathcal{X}}\) is the set of formulae containing the variables \(\mathcal{X}\).

Front: What does the semantic function \(⟦D⟧: \mathcal{D} \mapsto \mathcal{D}\) do, given a vector of subsets of \(\textbf{Proc}\) \((S_1, \dots, S_n)\) and a vector of formulae \(F_{X_i}\)?
Back: It maps each \(S_i\) to the set of processes satisfying \(F_{X_i}\), that is \(\mathcal{O}_{F_{X_i}}(S_1, \dots, S_n)\).

Front: In mutually recursive equational systems, how is \(\mathcal{O}_F\) defined?
Back: Exactly as in recursive HML, with the addition that \(\mathcal{O}_{X_i}(S_1, \dots, S_n)=S_i\).

The names of the SOS rules are
• ACT (action prefixing)
• SUM_j (process choice)
• COM{1,2,3} (process communication)
• RES (process interaction restriction)
• REL (label renaming)
• CON (process definition)