Both specifications and implementations can be represented by means of models of concurrency such as labelled transition systems (LTSs) or process graphs. I present the definitions below.
Another way to represent concurrent systems is by means of process algebraic expressions.
These concepts will be illustrated by means of an example (see below). It shows how an implementation could be given as a parallel composition of components, enforcing synchronisation on certain actions.
When both specifications and implementations are given as LTSs, we need a criterion to determine if they match. I will discuss a criterion based on bisimulation, that matches the states of the related LTSs. I show why it is useful here to abstract from internal actions of the implementation.
When the specification and implementation are given as process expressions, to decide whether they match, one considers the meaning, or semantics of these expressions. Often, this meaning is given by mapping them to LTSs.
J.C.M. Baeten & W.P. Weijland (1990): Process Algebra, Cambridge University Press
or
W.J. Fokkink (2000): Introduction to Process Algebra, Texts in Theoretical Computer Science, An EATCS Series, Springer.
The syntax of ACP, the Algebra of Communicating Processes, features the operations
Here are the definitions of these operators, in terms of process graphs extended with a predicate ✔ that signals successful termination.
There are two runners R_{1} and R_{1}
participating in the relay race, and while running they carry a baton.
Runner 1 starts running, and at the halfway-point passes the baton to
runner 2, who is waiting there. Then runner 2 runs the rest of the
race and delivers the baton at the finish.
We can describe the behaviour of the two runners by the ACP expressions:
In this course I will present a lattice of semantic equivalence relations on process graphs. These represent different points of view on whether two processes are roughly the same. In such a lattice, equivalences are classified with respect to their discriminating power.
Two processes p and q are partial trace equivalent, notation P =_{PT} Q, if they have the same partial traces. Here a partial trace of a process p is the sequence of transition labels encountered on a path in the process graph of p, starting from the initial state. Here a path can be defined as an alternating sequence of states and transitions, where each transition goes from the state before it to the state after it.
Processes p and q are completed trace equivalent, notation P =_{CT} Q, if moreover they have the same complete traces. Here a completed trace is a state that stems from a maximal path; one that cannot be prolonged at the end.
A completed trace of p is the sequence of labels of the transitions in a complete path. We write CT^{fin}(p) for the set of finite completed traces of process p, and CT^{∞}(p) for the set of all finite completed traces of p together with its infinite traces. When writing just CT(p) it depends on context which of the two is meant (i.e. this differs from one paper to the next). I this class I defined CT(p) to mean CT^{∞}(p).
Partial traces are defined likewise, but can end anywhere. We write PT^{fin}(p) for the set of finite partial traces of process p, and PT^{∞}(p) for the set of all finite partial traces of p together with its infinite traces. Normally, PT(p) means PT^{fin}(p).
Now processes p and q are infinitary completed trace equivalent, notation P =_{CT}^{∞} Q, if CT^{∞}(p) = CT^{∞}(q). It is a theorem that this implies that also PT^{∞}(p) = PT^{∞}(q). Processes p and q are finitary completed trace equivalent, notation P =_{CT}^{fin} Q, if CT^{fin}(p) = CT^{fin}(q) and PT^{fin}(p) = PT^{fin}(q). Here the last requirement cannot be skipped.
Likewise, processes p and q are infinitary partial trace equivalent, notation P =_{PT}^{∞} Q, if PT^{∞}(p) = PT^{∞}(q). They are finitary partial trace equivalent, notation P =_{PT} Q, if PT(P) = PT(Q).
Together, these four equivalence notion form a square when ordered w.r.t. discriminating power.
The definitions of partial and completed trace equivalence we encountered above can all be regarded as definitions of strong partial trace equivalence and strong partial completed trace equivalence, as long as we treat τ like any other action. To arrive at definitions of weak partial trace equivalence (=_{WPT} or =_{WPT}^{∞}), we define a weak partial trace of a process p as a strong partial trace of p from which all the occurrences of τ have been omitted. Now two processes are called (finitary or infinitary) weak partial trace equivalent if they have the same (finite or possibly infinite) weak partial traces. Weak completed trace equivalence, and its infinitary version, can be defined in the same vein.
In addition, two processes are called language equivalent if they have the same traces leading to terminating states. In automata theory such traces are called words, accepted by a process p. The set of all words accepted by p is the language accepted by p. It turns out that language equivalence is coarser than partial trace equivalence, whereas completed trace equivalence is finer than partial trace equivalence.
My paper The Linear Time - Branching Time Spectrum I is a small encyclopedia of (strong, or concrete) equivalence relations; language equivalence appears in Section 19.
I discuss why one would want to distinguish the processes b + c and τ.b+τ.c. The reason is that in a context of an environment that admits synchronisation on b, but not on c, the first process always performs the (weak) trace b, whereas the second has the possibility to reach a state of deadlock after doing the internal step τ. Deadlock is a (bad) state of a system, in which no further actions are possible, and the system does not terminate successfully.
For the same reason, one would want to distinguish the systems Q := τ.(b + c) and P := τ.b+τ.c. However, these two systems are equivalent under each of the 8 variants of trace equivalence discussed above. For this reason we need equivalence relations on process graphs or labelled transition systems that are finer than partial or completed trace equivalence, in the sense that they make more distinctions.
The definition of bisimulation equivalence, also called bisimilarity, can be found in this handout, which you should read entirely, except for the sections "Modal logic", "Non-well-founded sets" and "Concurrency". In that handout, LTSs and process graphs have an extra component ⊨ that is used to tell whether certain predicates, taken from a set P, hold in certain states of our processes. In this course, we typically consider only one predicate, namely ✔, telling that successful termination is possible in a state. For this reason, a quadruple (S,I,→,⊨) is presented as (S,I,→,✔). More commonly, one ignores the component ⊨ or ✔ completely.
On the set of all process graphs we can study multiple equivalence relations and order them w.r.t. their discriminating power. I drew a spectrum of equivalence relations, with finer ones located above coarser ones.
In this spectrum I located partial trace equivalence, completed trace equivalence and bisimulation equivalence, and treated examples showing their differences. Bisimulation equivalence is at the top of the spectrum and partial trace equivalence near the bottom. Completed trace equivalence is somewhere in between. Bisimulation equivalence is called a branching time equivalence, because it takes into account at which point two different traces branch off. Partial and completed trace equivalence on the other hand are linear time equivalences, as they only focus on the linear executions of a process, without taking branching into account.
The spectrum of weak trace equivalences is the same as in the strong case: weak completed trace equivalence is finer (more discriminating) than weak partial trace equivalence. A weak version of bisimilarity is even finer.
Defining a weak form of bisimilarity is relatively tricky. As we saw by example, just contracting all τ-moves in a labelled transition system doesn't yield what we want to get. There are several, subtly different, approaches in the literature. The most prominent ones are weak bisimilarity and branching bisimilarity, both defined in the above-linked handout.
A colouring of a labelled transition system is just a function that associates a colour with every state. (Thus a colouring induces an equivalence relation on states, and any equivalence relation induces a colouring.) Now given a colouring, the potentials of a state s of a certain colour, are all pairs (a,C) with a an action and C a colour, such that s can do some inert transitions followed by an non-inert a-transition to a state with colour C. Here a transition is inert if it is labelled τ and moreover goes between two states of the same colour. Thus if (a,C) is a potential of a state s, then either a≠τ or C is not the colour of s. The colouring is consistent if all states of the same colour also have the same potentials. Now one can show that two states are branching bisimulation equivalent iff there exists a consistent colouring that gives them the same colour.
Strong bisimilarity can be characterised in the same way; the only difference is that no actions count as inert. Thus a potential (a,C) simply means one can do an a-transition to a state with colour C.
An alternative approach is to introduce variables X,Y,Z to the language, as well as recursion constructs <X|S>. Here S is a set of recursive equations X = P_{X}, and <X|S> specifies "the process X that satisfies the equations S". We normally restrict attention to the guarded case, in which there is only one process X satisfying S.
Here are the definitions, in terms of process graphs without predicates and without a notion of final states, of the operators mentioned above:
The main differences between ACP and CCS are:
In the operational framework we drop the distinction between processes and states. There will be one humongous LTS (without initial state) whose states are all possible closed process expressions, and the transitions between states are given by certain operational rules. To get an idea of the difference between process graphs and LTSs, read the definitions in the bisimulation handout, and especially note how Definition 3 of bisimulation avoids having the clause on initial states.
Today I introduce the approach of structural operational semantics (SOS), by giving the structural operational semantics of CCS. Read the first section of this handout. In SOS, the outgoing transitions of a composed process will be determined out of the outgoing transitions of its argument processes without at that time considering transitions occurring further on. What is called $\textbf{fix}_XS$ in the handout is called <X|S> in class. The rule for recursion involves substitution.
To formulate a canonical safety property, assume that our alphabet of visible actions contains one specific action $b$, whose occurrence is bad. The canonical safety property now says that $b$ will never happen.
Definition: A process $p$ satisfies the canonical safety property, notation $P \models \textit{safety}(b)$, if no trace of $P$ contains the action $b$.
In this definition it makes no difference whether "trace" refers to a partial or a complete trace, whether infinite traces are taken into account or not, or whether we use strong or weak traces. I often use words like "trace" instead of "possibly infinite strong partial trace" when the choice of adjectives is irrelevant.
To arrive at a general concept of safety property for labelled transition systems, assume that some notion of bad is defined. Now, to judge whether a process $P$ satisfies this safety property, one should judge whether $P$ can reach a state in which one would say that something bad had happened. But all observable behaviour of p that is recorded in a process graph until one comes to such a verdict, is the sequence of visible actions performed until that point. Thus the safety property is completely determined by the set of sequences of visible actions that, when performed by $P$, lead to such a judgement. Therefore one can just as well define the concept of a safety property in terms of such a set.
Definition: A safety property of processes in an LTS is given by a set $B \subseteq A^*$. A process $P$ satisfies this safety property, notation $P \models \textit{safety}(B)$, when $\textit{WPT}(P) \cap B = \emptyset$.
The following theorem says that weak partial trace equivalence preserves safety properties.
Theorem: If $P =_{\textit{WPT}} Q$ and $P \models \textit{safety}(B)$ for some $B \subseteq A^*$, then also $Q \models \textit{safety}(B)$.
Thus, if two processes have the same weak partial (finite) traces then they satisfy the same safety properties. The reserve also holds: if two processes satisfy the same safety properties, then they have the same weak partial traces. In class I sketched a proof of these (obvious) statements.
A liveness property says that something good will happen eventually. The terminology "liveness" used here stems from Lamport 1977, who was inspired by the older use of the term "liveness" in Petri nets, whose meaning however is different. The following concepts are important when formulating (or proving) liveness properties.
WPT^{fin} | |||
P | normal progress | a.g.0 | $\{ag,a,\epsilon\}$ |
Q | fair divergence | a.Δg.0 | $\{ag,a,\epsilon\}$ |
R | livelock | a.(g.0+ τ.Δ0) | $\{ag,a,\epsilon\}$ |
S | deadlock | a.(g.0 + τ.0) | $\{ag,a,\epsilon\}$ |
In the above table, the unary operator $\Delta$ appends a $\tau$-loop at the beginning of its argument. Formally, $\Delta G$ is the process graph created out of $G$ by adding a fresh initial state $I$, together with a fresh $\tau$-loop I --$\tau$--> I, and a transition I --$\alpha$--> s for each transition I_{G} --$\alpha$--> s from $G$. Process graphs of the 4 processes in the above table are drawn in class. If we assume fairness, "normal progress" may be identified with "fair divergence", but in the absence of a fairness assumption only "normal progress" satisfies the liveness property that g will happen eventually. In weak partial trace semantics, deadlock, livelock, divergence and normal progress are all identified. The weak partial traces of all four processes are the same. This week it is homework to invent definitions of completed trace equivalence that make different choices in this matter.
In CSP, as well as in David Walker's version of weak bisimulation semantics, livelock and divergence are identified, and distinguished from deadlock and normal progress, thereby implicitly assuming choices to be unfair (a safe worst case scenario). In weak and branching bisimulation semantics as used in CCS and ACP, choices are assumed to be fair, and fair divergence is identified with normal progress, and distinguished from livelock. Moreover, there is no distinction between deadlock and livelock. This helps in the verification of communication protocols, where you try to send a message as long as needed until it succeeds and assume it will eventually arrive correctly.
Divergence-preserving branching bisimilarity ($BB^\Delta$) is the finest useful weak equivalence found in the literature. It distinguishes all four modes of progress: deadlock, livelock, possibly fair divergence and normal progress. It can be defined in terms of consistent colourings:
A colouring of a labelled transition system is just a function that associates a colour with every state. (Thus a colouring induces an equivalence relation on states, and any equivalence relation induces a colouring.) Now given a colouring, the potentials of a state s of a certain colour, are all pairs (a,C) with a an action and C a colour, such that s can do some inert transitions followed by an non-inert a-transition to a state with colour C. Here a transition is inert if it is labelled τ and moreover goes between two states of the same colour. Thus if (a,C) is a potential of a state s, then either a≠τ or C is not the colour of s. The colouring is consistent if all states of the same colour also have the same potentials. Now one can show that two states are branching bisimulation equivalent iff there exists a consistent colouring that gives them the same colour. (Until here repeated from last week.)
State s is internally divergent w.r.t. a colouring if there is an infinite path of τ-transitions starting from s, only passing through states with the same colour as s. The colouring preserves internal divergence if for any colour either all states of that colour are divergent w.r.t. the colouring, or none are. Now two states are divergence-preserving branching bisimulation equivalent if they receive the same colour by some consistent colouring that preserves internal divergence.
State s is divergent if there is an infinite path of τ-transitions starting from s. A colouring preserves divergence if for any colour either all states of that colour are divergent, or none are. Now two states are weakly divergence preserving branching bisimilar if they receive the same colour by some consistent colouring that preserves divergence. In class I sketch a proof that this notion is weaker than (or possibly equal to) divergence preserving branching bisimilarity, in the sense that when two processes are divergence preserving branching bisimilar, then they are surely weakly divergence preserving branching bisimilar.
Divergence-preserving weak bisimilarity ($WB^\Delta$) is defined much simpler: A divergence-preserving weak bisimulation is one that relates divergent states to divergent states only. Here a state is divergent if it is the start of an infinite path, all of whose transitions are labelled τ.
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.
It is not hard to show that (strong) partial trace equivalence is a congruence for encapsulation. This follows because the partial traces of ∂_{H}(P) are completely determined by the partial traces of the process P itself (namely by removing all partial traces with actions from H). The same argument can be used to see that partial trace equivalence is a congruence for all operators of CCS and ACP.
Partial trace equivalence is inadequate to deal with deadlock. Adding deadlock information to partial trace semantics yields completed trace semantics. However, completed trace equivalence is not a congruence for all operators. It fails for the restriction operator of CCS, which is the same as the encapsulation operator of ACP. It also fails for the parallel composition of CSP. A counterexample: the processes $a.b + a.c$ and $a.(b+c)$ are completed trace equivalent. However, after placing them in a context $\partial_H(\_\!\_)$ with $H=\{c\}$, they are not. For $\partial_H(a.b + a.c)$ has a completed trace $a$, yet $\partial_H(a.(b+c))$ does not. This operator corresponds to placing the processes in an environment that blocks, or refuses to synchronise on, the action $c$. Strong bisimulation equivalence on the other hand is a congruence for all operators of ACP, CCS and CSP. This is a reason to use bisimulation rather then partial or completed trace equivalence.
The congruence closure ~^{c} of ~ (w.r.t. a language L) is defined by
P ~^{c} Q if and only if C[P] ~ C[Q] for any L-context C[ ].
It can be shown that ~^{c} is the coarsest congruence finer than ~. (Note that there are three statements in that last sentence.)The congruence closure of strong completed trace equivalence can be characterised as strong failures equivalence (not defined yet). It is finer than strong completed trace equivalence, but coarser than strong bisimilarity. A similar thing applies to weak equivalences.
Expansion Theorem for CCS: Let $P := \sum_{i\in I}\alpha_i.P_i$ and $Q := \sum_{j\in J}\beta_j.Q_j$. Then $$P | Q = \sum_{i\in I} \alpha_i (P_i | Q) + \sum_{j\in J} \beta_j (P | Q_j) + \sum_{\begin{array}[t]{c}i\in I, j \in J \\ \alpha_i = \bar\beta_j\end{array}}\tau.(P_i | Q_j).$$ By means of this theorem, and a similar treatment of the restriction and renaming operators of CCS, any CCS expression $P$ (with only guarded recursion) can be rewritten into a bisimulation equivalent CCS expression of the form $\sum_{i\in I}\alpha_i.P_i$. Such an expression is called a head normal form. In fact, this can be done in such a way, that the $P_i$ are exactly those processes with $P \stackrel{\alpha_i}{\Longrightarrow} P_i$. If there is no recursion at all, this process can be iterated, and any recursion-free CCS expression can be rewritten in to a Basic CCS expression: one built solely from 0, $+$ and action prefixing. The above complete equational axiomatisation of (strong) bisimulation equivalence for basic CCS now extends to a complete equational axiomatisation of all of recursion-free CCS.
Likewise, in CCS, weak branching bisimulation equivalence $=_{WB}$ is replaced by weak bisimulation congruence $=_{WB}^c$ It is defined as the coarsest congruence contained in $=_{WB}$, obtained as the congruence closure of $=_{WB}$ (see above). It turns out that $P =_{WB}^c Q$ iff for all processes $R$ we have $P+R =_{WB} Q+R$. Thus it suffices to take the congruence closure w.r.t. the +-operator; the result then turns out to be a congruence for the other operators as well.
In fact, the same can be done for all other equivalences we encountered (such as weak and strong completed trace equivalence) and in class I indicate the resulting congruence closures on the linear time - branching time spectrum, our map of equivalences, sorted by the "finer than"-relation.
Two processes P and Q are rooted branching bisimulation (RBB) equivalent iff
RBB equivalence equals branching bisimulation congruence; it is finer, i.e. more discriminating, than BB equivalence, and it is a congruence for all operators of ACP, CCS and CSP.
Similarly, I present another characterisation of $=_{WB}^c$, and illustrate it in class with examples:
Two processes P and Q are RWB equivalent iff
RWB equivalence equals weak bisimulation congruence; it is finer, i.e. more discriminating, than WB equivalence, and it is a congruence for all operators of ACP, CCS and CSP.
These above two rooted equivalences can be given a uniform treatment. Define a rooted weak or branching bisimulation to be one that relates roots (= initial states) with roots only. Now two processes are RBB (resp. RWB) equivalent iff after applying an operation (root-unwinding) that preserves strong bisimilarity and removes any loops going through the initial states they are related by a such a rooted weak or branching bisimulation.
Delay bisimilarity and η-bisimilarity are semantic equivalences intermediate between weak and branching bisimilarity, defined in the handouts. Rooted delay bisimilarity is axiomatised by (T1) and (T2); rooted η-bisimilarity by (T1) and (T3). Rooted branching bisimilarity is completely axiomatised by $$\alpha.(\tau.(P+Q)+Q) = \alpha.(P+Q)$$ on top the of axioms for strong bisimilarity. This axiom is a strengthening of (T1). There does not exists a congruence that is axiomatised by (T1) plus the axioms of strong bisimilarity alone. In this direction, rooted branching bisimilarity is at good as it gets.
The recursive specification $X = \tau.X$ has a unique solution up to strong bisimilarity, but not up to rooted weak or branching bisimilarity. So to make RSP work optimally, we need a more liberal concept of guardedness for strong bisimilarity (or other strong equivalences) than for weak bisimilarity (or other weak equivalences). In other words, we need a stronger, or less liberal, concept of unguardedness for strong bisimilarity.
We call a recursive specification strongly unguarded if a recursive variable $X$ occurs in the body of a recursive equation, but not in a subterm of the form $\alpha.P'$, that is, not guarded by $\alpha$, for any action $\alpha \in Act = A\cup \{\tau\}$. It is weakly unguarded if a recursive variable $X$ occurs in the body of a recursive equation, but not in a subterm of the form $a.P'$, that is, not guarded by $a$, for any visible action $a \in A$. Note that, in line with the meaning of the words "strong" and "weak", a strongly unguarded recursive specification is certainly also weakly unguarded. This wouldn't have worked out so nicely when talking about "guarded" rather than "unguarded" recursive specifications.
RSP is a sound principle for strong bisimulation semantics when interpreting "guarded" as "not strongly unguarded". But to make it a sound principle for weak or branching bisimulation semantics, we need to interpret "guarded" as "not weakly unguarded".
Again, it can be shown that for weak and branching bisimilarity, the axioms listed above, and the axioms that enable head normalisation, together with RDP and RSP, form a complete axiomatisation for processes without weakly unguarded recursion.
Weak bisimulation congruence, the congruence closure of weak bisimilarity, is the default semantic equivalence used in the language CCS. It can be characterised as rooted weak bisimilarity: two processes are weak bisimulation congruent, iff after applying an operation (root-unwinding) that preserves strong bisimilarity and removes any loops going through the initial states they are related by a rooted weak bisimulation, one that relates initial states with initial states only. Likewise, branching bisimulation congruence, the congruence closure of branching bisimilarity, is the default semantic equivalence used in the language ACP. It can be characterised as rooted branching bisimilarity.
The language CSP follows the other approach: it drops the offending operator +. Its operational semantics is given here.
The syntax of CSP, the theory of Communicating Sequential Processes, features the operations
Here are the definitions, in terms of process graphs without predicates and without a notion of final states, of the operators mentioned above:
Today I present the SOS of CCSP, also given here.
I also cover the use of negative premises in structural operational semantics (see the handout above) and the GSOS format with negative premises, using the priority operator that is sometimes added to ACP as an example.
Finally, I explain a theorem in Structured Operational Semantics, saying that strong bisimulation is a congruence as soon as all operators concerned have operational rules in the GSOS format. See the handout on structural operational semantics for details. In class I cover few examples illustrating a failure of bisimulation being a congruence when we deviate from this format.
As a consequence of this result, strong bisimilarity is a congruence for all operators of ACP, CCS and CSP.
In the lecture I illustrate this on an example. It also illustrates that each use of negation in the an HML formula correspond with a switch of initiative from one side to the other in the bisimulation game.
By the way: Please read this small fragment of the wikipedia page for bisimulation for a Game theoretical characterisation of strong bisimilarity. (This should have been mentioned in Lecture 3, but then I forgot.)
Above, the red connectives and modalities are redundant, because they are expressible in the green connectives and negation. Likewise, the green connectives are expressible in terms of the red ones and negation. Finally, if we keep both the red and the green connectives and modalities, then negation is redundant. It is the latter form we need to extend HML into the modal $\mu$-calculus. It additionally has modalities $\mu X.\phi(X)$ and $\nu X.\phi(X)$. Here $\phi(X)$ is a modal $\mu$-formula that may contain the variable $X$. $\mu X.\phi(X)$ denotes the least fixed point of the equation $X=\phi(X)$, and $\nu X.\phi(X)$ the greatest. For these fixed points to exist, the formulas $\phi(X)$ need to be monotone in $X$, and to achieve that we needed to eliminate negation.
A formal denotational semantics of the modal $\mu$-calculus can be found in wikipedia. There, negation is not eliminated, but instead a variable needs to be under an even number of negation operators. This treatment is equivalent. In the lecture I merely mentioned the modal $\mu$-calculus, so that you know it exists. For now it is not covered material, on which I may ask exam questions.
P ⊨ $\top$ | ||
P ⊭ $\bot$ | ||
P ⊨ Φ∧Ψ | iff | P ⊨ Φ and P ⊨ Ψ |
P ⊨ Φ∨Ψ | iff | P ⊨ Φ or P ⊨ Ψ |
P ⊨ [K]Φ | iff | ∀Q∈{P':P--a-->P' and a∈K} . Q ⊨ Φ |
P ⊨ <K>Φ | iff | ∃Q∈{P':P--a-->P' and a∈K} . Q ⊨ Φ |
Preorders are used just like equivalence relations to compare specifications and implementations. I normally write the implementation on the right: $$\textit{Spec} \sqsubseteq \textit{Impl}$$ For each preorder $\sqsubseteq$ there exists an associated equivalence relation $\equiv$, called its kernel. It is defined by $$P \equiv Q ~~\Leftrightarrow~~ (P \sqsubseteq Q \wedge Q \sqsubseteq P).$$ Preorders play the same role as semantic equivalence relations, and can be ordered in a spectrum. In fact, for almost every semantic equivalence $\equiv$, there exists an associated preorder with the property that $\equiv$ is its kernel. The partial trace preorder for instance is defined by $$P \sqsubseteq_{\it PT} Q ~~\Leftrightarrow~~ PT(P) \supseteq PT(Q)$$ Half of the scientists orient the symbol $\sqsubseteq_{\it PT}$ in the other direction, so that it aligns with the direction of the set-inclusion symbol $\subseteq$. I aligned this course reversely. The process $Q$ in $P \sqsubseteq Q$ is called a refinement of $P$. It is a step closer to the implementation. We require that all good properties of process $P$ are shared by $Q$, although it is acceptable if $Q$ has extra good properties, not required by $P$. Most of the time, our properties will be trace based, such as
In such cases, a process is defined to have the good property $\phi$ iff each of its (complete) traces has the good property $\phi$. Thus if process $Q$ has only a subset of the traces of $P$, it surely has all the good properties of $P$. One has to be careful with this type of reasoning, and not jump to the conclusion that a process that cannot do anything is surely the best of all. But it motivates the orientation of the symbol $\sqsubseteq$, with the improved process on the right.
When adding simulation equivalence to the spectrum of equivalence relations that had already partial trace equivalence, completed trace equivalence and bisimulation equivalence in it, it turns out that simulation equivalence is finer that =_{PT}, coarser than =_{B}, and incomparable with =_{CT}.
Let $L$ be the fragment of the infinitary Hennessy-Milner logic, given by the syntax \[\varphi ::= {\color{green} \top} \mid {\color{green} \bigwedge_{i\in I} \varphi_i} \mid {\color{green} \langle \alpha \rangle \color{green}\phi} \] This logic yields a modal characterisation of (strong) simulation equivalence, just like the full Hennessy-Milner logic yields a model characterisation of (strong) bisimulation equivalence: \[ P =_ S Q ~~\Leftrightarrow~~ \forall \varphi \in L.~ (P \models \varphi \Leftrightarrow Q \models \varphi). \]
[BK08] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. ISBN 978-0-262-02649-9
I will not say much about CTL*, a logic that combines the expressive power of LTL and CTL.
I also extend the above results to LTSs that may have deadlocks (states without outgoing transitions). There are several approaches found in the literature:
Two processes $P$ and $Q$ (in an arbitrary LTS) satisfy the same LTL formulas if P =_{CT}^{∞} Q. For finitely-branching processes, we even have "iff".
Two processes $P$ and $Q$ (in an arbitrary LTS) satisfy the same LTL_{-X} formulas if P =_{WCT}^{∞} Q, that is, if they have the same (possibly infinite) weak completed traces (obtained by leaving out τ's).
Two processes $P$ and $Q$ (in an arbitrary LTS) satisfy the same CTL formulas if they are strongly bisimilar. For finitely-branching processes, we even have "iff". For general processes, we also have "iff", provided that we use CTL with infinite conjunctions.
Two processes $P$ and $Q$ (in an arbitrary LTS) satisfy the same CTL_{-X} formulas if they are divergence-preserving branching bisimilar. We even have "iff", provided that we use CTL_{-X} with infinite conjunctions.
The last result, however, only works with approach 3 or 4 above. Otherwise we would get a weaker form of divergence-preserving branching bisimilarity, which would identify deadlock and livelock.
The complexity of the original algorithm, by Kanellakis & Smolka, is $O(m.(n+l))$, where $m$ is the number of transitions, $n$ is the number of states, and $l$ is the number of different action labels in a finite system (when assuming n < m+2, which can be achieved by collapsing deadlock states). (Often $l$ is taken to be a constant, and not counted.) The algorithm has been improved by Paige & Tarjan to reach complexity $O(m.(log(n)+log(l))$.
Note however, that the complexity of deciding bisimilarity is EXPTIME when the input is a process algebra expression (of a not too complex kind). This is because an LTS can be exponentially larger than its generating expression.
The partition refinement algorithm works by first considering all processes equivalent, and putting them into 1 big equivalence class. Then we keep finding reasons for cutting an equivalence class into two smaller equivalence classes (red and blue), namely when we find evidence that none of the process in red are equivalent to processes in blue. When we run out of reasons to further cut equivalence classes in two, the equivalence relation we are left with is strong bisimilarity.
There are two crucial differences with the partition refinement algorithm for strong bisimilarity:
That book uses equational reasoning (applying axioms) to show that the implementation is rooted branching bisimilar to the specification. This mode of proving things is called equivalence checking. Another form of equivalence checking is to directly show the rooted branching bisimilarity of the transition systems of Spec and Impl, for instance using the partition refinement algorithm. An alternative to equivalence checking is model checking. This also involves modelling the (implementation of) the protocol in a process algebra or similar formalism, but instead of developing an abstract specification, one formalises intended properties in terms of temporal logics, like CTL or LTL. Then one applies techniques to directly show that the (transition system generated by the) implementation of the protocol satisfies its temporal formula. Out of the 8 major toolsets for system verification surveyed here, 7 employ model checking and 4 employ equivalence checking. Two of the latter use rooted branching bisimulation as their primary equivalence. A more complete overview of tools is found on pages 92-95 of the above book.
Of course equivalence checking and model checking can be combined: there are theorems that tell us that if Spec ~ Impl for a suitable equivalence ~, and Spec satisfies a temporal formula of a particular form, then also Impl satisfies this formula. Using such results, we can first use equivalence checking or partition refinement to replace a system with many states by a smaller system that is semantically equivalent. Then we use model checking to check that the smaller system satisfies a correctness property, given by a temporal formula. We then know that also the original system satisfies this correctness property.
The correctness of the alternating bit protocol (ABP) hinges on a fairness assumption, saying that if you try to send a message infinitely often, sooner or later it will come through correctly. Without relying on such an assumption, the protocol is obviously incorrect, on grounds that there can be no way to ensure correct message delivery. Fairness assumptions are important in verification. If we refuse to make them we declare any protocol like the ABP a priori incorrect, and miss an opportunity to check the protocol logic for flaws that have nothing to do with the unreliable nature of the communication channel.
A strong fairness assumption is already incorporated in the notions of (rooted) branching (or weak) bisimulation equivalence seen before. No fairness assumption is incorporated in divergence-preserving (rooted) branching (or weak) bisimulation equivalence (see lecture 5). Those equivalences would not be suitable for the verification of the ABP.
Orthogonal to this classification is a spectrum that ranges from interleaving semantics, in which parallelism is treated by arbitrary interleaving of atomic actions, and causality respecting semantics, in which causal relations between actions are explicitly taken into account. A typical equation that holds in interleaving semantics but not in causal semantics is a||b = ab+ba. It is rejected in causal semantics because in a||b the two actions a and b are causally independent, whereas in ab+ba either a depends on b or vice versa. A causal version of partial trace equivalence can be obtained by taking partial orders of actions instead of sequences. This is why causal semantics are sometimes called partial order semantics.
Between interleaving and causal semantics lays step semantics. It differs from interleaving semantics by explicitly taking into account the possibility that two concurrent actions a and b by pure chance happen at the exact same (real-time) moment. Here a||b differs from ab+ba because only the former has a trace where a and b happen at exactly then same time.
Between step semantics and causal semantics lays interval semantics. It takes causality into account only to the extend that it manifest itself by durational actions overlapping in time.
One argument to use at least interval semantics (and possibly causal semantics) instead of interleaving semantics is real-time consistency. If we imagine that actions take time to execute, interleaving semantics may equate processes that have different running times (it is not real-time consistent), whereas this cannot happen in interval or causal semantics. An other argument is action refinement: we want that two equivalent processes remain equivalent after systematically splitting all occurrences of an action a into a1;a2, or refining a into any more complicated process. This works for interval or causal semantics, but not for interleaving semantics.
A map of the equivalences discussed above appears on page 3 of this paper. In this class I will not treat the right-most column of that diagram. Please also read the text of page 3 below that diagram. And read section 1.2 (on pages 4-5), listing reasons for preferring one semantic equivalence over another.
Petri nets can be translated to process graphs by taking as states their markings, the initial marking being the initial state, and as process-graph transitions the transition firing relation between markings. A theorem states that translating an ACP or CCS expression into a net, and then translating further into a process graph, yields the same graph, up to strong bisimilarity, as directly interpreting the expression as a process graph (using the standard denotational or operational semantics).
On Petri nets and event structures it is common to not use interleaving equivalences that identify a|b and ab+ba. Reasons to distinguish these processes are preservation of semantic equivalence under action refinement and real-time consistency; see above.
In the same spirit, a common and simple kind of safety property can be modelled in LTL as $\neg$Fb, or equivalently G$\neg$b. It says that there is no path from the initial state to a state where b holds. Here $b$ is an atomic proposition assigned to those states in the Kripke structure that are deemed "bad".
Safety properties are often established by means of invariants, properties of states that hold in the initial state, and are preserved under doing a transition. Being "not a bad state" could be such an invariant. Note that if the initial state is "not bad", and each transition that starts in a "not bad" state also ends in a "not bad" state, then indeed it follows that no bad state in reachable, and $\neg$Fb holds. In the formulation of invariants, states are often determined by the values of certain variables, and the invariants are formulated in terms of these variables. The bad thing might be that variable $x$ exceeds the value 137.
Whereas normally this course focuses on reactive systems, where visible actions model a synchronisation between the modelled system and its environment, today I focus on closed systems, which are not supposed to be influenced by their environment. In a reactive system, represented as a process graph, the labelling of the transitions provides an interface for the environment to interact with the system; the environment (or user) can either block or allow a certain action, and thereby steer the system when it has a choice between multiple actions. In Kripke structures the transitions are not labelled, and it is much more common to study closed systems. If in this setting one wants to model the interaction of our system with a user, it is more appropriate to model the user separately, and put this user model in a parallel composition with the system under investigation.
Whether liveness properties of systems hold depends often on whether or not we make appropriate progress and fairness assumptions. I discuss 5 such assumptions: progress, justness, weak fairness, strong fairness and full fairness. Please read page 7 of this paper for an informal description of the first four of these assumptions, and an illustrating example.
A linear-time property is a property of paths. LTL is a logic that specifies properties of paths in Kripke structure. Therefore any LTL formula models a linear-time property. A good example of a linear-time property is given by the LTL formula Fg discussed above. It says that a state that is labelled by the atomic proposition $g$ occurs on this path. But we can talk about linear-time properties also if they are specified informally, or using some other formalism.
Now I define what it means for a process $P$ to satisfy the linear-time property $\varphi$ under the completeness criterion $C$. This is denoted $P \models^C \varphi$. It holds if all complete paths of $P$ satisfy $\varphi$. Here a complete path is one that is selected as being complete by the completeness criterion $C$.
In a Kripke structure one normally assumes that there are no states without outgoing transitions. In the world of LTSs without a termination predicate, this condition is called deadlock-free, for a state without outgoing transitions is regarded as a deadlock. For such Kripke structures, the default completeness criterion says that a path is complete if and only if is infinite. If no other completeness criterion is discussed, this is always the intended one. Under this completeness criterion, formulas $\varphi$ holds for process $P$ iff it holds for all infinite paths of $P$. Naturally, $P \models^C \varphi$ can then be abbreviated by $P \models \varphi$. The superscript $C$, and the entire concept of a completeness criterion, need to come up only when we want to discuss alternative completeness criteria.
In LTSs, or in Kripke structures that are explicitly allowed to contain deadlock states, the default completeness criterion says that a path is complete if it is either infinite or ends in a state from which no further transitions are possible. This is the completeness criterion used when defining completed trace semantics―see Lecture 2.
We say that completeness criterion $D$ is stronger than completeness criterion $C$ if it rules our more paths as incomplete, that is, if the set of complete paths according to $D$ is a subset of the set of complete paths according to $C$. If $D$ is stronger than $C$, then $P \models^C \varphi$ implies $P \models^D \varphi$, but not necessarily vice versa. For to check $P \models^D \varphi$, we have to check that $\varphi$ holds for all complete paths, and under $D$ there are fewer complete paths than under $C$, so there is less to check.
Now progress, justness, weak fairness and strong fairness can be seen as completeness criteria, ruling out some paths from consideration when determining whether a process satisfies a property. They get stronger in the listed order, so $P \models^{\it SF} \varphi$ implies $P \models^{\it WF} \varphi$, which implies $P \models^J \varphi$, which implies $P \models^{\it Pr} \varphi$, for all processes $P$ and properties $\varphi$. Here $\it SF$, $\it WF$, $J$ and $\it Pr$ are the completeness criteria formalising those assumptions.
The strongest completeness criterion thinkable (let me call it $\infty$ in this paragraph only) says that no path is complete. Naturally, we now have $P \models^\infty \varphi$ for all processes $P$ and properties $\varphi$. This is not a useful completeness criterion, so we now forget it again.
The weakest completeness criterion possible (let me call it $\emptyset$) says that all paths are complete. This is in fact a useful completeness criterion. Note that $P \models^{\it Pr} \varphi$ implies $P \models^\emptyset \varphi$, so we have already a hierarchy of 5 completeness criteria.
A task $T$ is enabled is a state $s\in S$, if $s$ has an outgoing transition that belongs to that task. Task $T$ is perpetually enabled on a path $\pi$ if it is enabled in every state of $\pi$. Task $T$ occurs in $\pi$ if $\pi$ contains a transition that belongs to $T$.
A finite prefix of a path $\pi$ is the part of $\pi$ from its beginning until a given state. A suffix of a path $\pi$ is the path that remains after you remove a finite prefix of it. Note that if $\pi$ is infinite, then all its suffixes are infinite as well.
A path $\pi$ is called weakly fair if, for every suffix $\pi'$ of $\pi$, each task that is perpetually enabled on $\pi'$, occurs in $\pi'$.
Equivalently: A path $\pi$ is weakly fair if each task that from some state onwards is perpetually enabled on $\pi$, occurs infinitely often in $\pi$.
Weak fairness is a completeness criterion: the weakly fair paths are the complete ones.
Weak fairness as a property of paths can be expressed by the LTL formulas $${\bf G}({\bf G}(\textit{enabled}(T)) \Rightarrow {\bf F} (\textit{occurs}(T)))$$ for each task $T$. Hence $\textit{enabled}(T)$ is an atomic proposition that is assigned to a state from which a transition from $T$ is enabled. Likewise $\textit{occurs}(T)$ holds for a Kripke state modelling an LTS transition from $T$. The above formula can equivalently be written as $${\bf G}(\neg {\bf G}(\textit{enabled}(T) \wedge \neg \textit{occurs}(T)))$$ or $${\bf FG}(\textit{enabled}(T)) \Rightarrow {\bf GF}(\textit{occurs}(T)).$$ The statement $P \models^{\it WF} \varphi$ is equivalent to $P \models \chi \Rightarrow \varphi$, where $\chi$ is the conjunction of the formulas above, one for each task $T$.
A path $\pi$ is called strongly fair if, for every suffix $\pi'$ of $\pi$, each task that is relentlessly enabled on $\pi'$, occurs in $\pi'$.
Equivalently: A path $\pi$ is strongly fair if each task that is relentlessly enabled on $\pi$ occurs infinitely often in $\pi$.
Also strong fairness is a completeness criterion: the strongly fair paths are the complete ones. Note that a task that is perpetually enabled is certainly relentlessly enabled. Hence a strongly fair path is surely also weakly fair. Thus strong fairness is a stronger completeness criterion than weak fairness.
As an example, take the alternating bit protocol (ABP) encountered in Lecture 12. A property that this protocol should satisfy is that each message $d\in D$ that is offered by the user of the protocol on channel $A$ will eventually be delivered to the user at the other end via channel $C$. In LTL, implicitly applying the translation from process graphs to Kripke structures discussed in Lecture 10,
Let us consider the successful transmission of a message over the unreliable channel to be a task. If we look at the process graph of the ABP, there are infinite paths that get stuck in loops, and in which (from some point onwards) the successful sending of a message does not occur. Looking at the process graph, we see that our task is relentlessly enabled on such a path, but not perpetually enabled. Hence such a path is weakly fair but not strongly fair. It follows that the ABP is correct when we make a strong fairness assumption, but not when we only make a weak fairness assumption.
Strong fairness can be expressed in LTL as $${\bf G}({\bf GF}(\textit{enabled}(T)) \Rightarrow {\bf F} (\textit{occurs}(T)))$$ The above formula can equivalently be written as $${\bf G}(\neg {\bf G}({\bf F}(\textit{enabled}(T)) \wedge \neg \textit{occurs}(T)))$$ or $${\bf GF}(\textit{enabled}(T)) \Rightarrow {\bf GF}(\textit{occurs}(T)).$$
To model local fairness assumptions, we need to explicitly declare our tasks. This means that we move from process graphs or Kripke structures to the extension of these structures with the tasks as an extra component.
A global fairness assumption, on the other hand, is independent of the system under investigation, and instead considers all choices of a given type to be fair. Here we work with models of concurrency that are equipped with some structure, and when translating those models to process graphs or Kripke structures, the Tasks are somehow extracted from the structure of the original model.
An example is fairness of actions. Here the underlying model of concurrency consists of process graphs, where the transitions are labelled with actions. Now there is a task for each action, and a transition belongs to that task if it has the corresponding label.
Another example is fairness of transitions. Here each transition constitutes a singleton task.
A third example is fairness of instructions. Here the underlying model is a programming language, where each program is translated to a process graph or Kripke structure. Now there is a task for each line of code (instruction) in the source program, and a transition in the process graph belongs to that task iff it stems from that instruction.
There are more such methods, but I will skip them here.
When dealing with weak or strong fairness, it is often common to put each transition in at least one task. One way to accomplish this is to create one special task that contains all transitions. In this situation, a weakly (or strongly) fair path is certainly progressing. Namely, if a path $\pi$ is not progressing (fails the progress condition), then it ends in a state with an outgoing transition. Hence a task $T$ containing that transition is perpetually enabled in the suffix $\pi'$ of $\pi$ consisting of its last state only. Now weak fairness prescribes that task $T$ occurs in $\pi'$, which it clearly doesn't. So $\pi$ is not weakly fair.
This arguments shows that weak (as well as strong) fairness is a stronger completeness criterion than progress.
A progress assumption is build in in the logics CTL and LTL (for they work with infinite paths rather than partial paths).
Now if we considered $X$ it is own right, the assumption of progress would guarantee that $X$ will eventually do an $a$-action. It cannot stay in its initial state. However, in the context with the parallel process $Y$, the composition $X||Y$ is not guaranteed to ever do an $a$, at least when only assuming progress. For the infinite path that consists of $b$-transitions only does satisfy the progress condition.
Now justness allows us to apply progress locally, and conclude that also $X||Y$ must eventually do an $a$-action, at least when assuming that $X$ and $Y$ are parallel components that do not interact with each other in any way.
Formally, justness can be formulated in terms of resources needed by transitions. These resources could be components in a parallel composition that give rise to the transition. The process $a|\bar a$ for instance has two components, R(ight) and L(eft). The $a$-transitions needs one recourse, namely L. Likewise, the $\bar a$-transition only needs R. However, the $\tau$-transitions needs two resources, namely L and R. In the setting of Petri nets, the resources needed by a transition are the tokens that need be in its preplaces.
Now a path is called just if for each transition that is at some point enabled (meaning it is an outgoing transition of a state in the path), one of its resources is actually used for a transition that occurs in the path (past that state).
The rough idea is that if all resources for a transition are present, and none is ever used for anything else, then the transition ought to occur.
To this end we only have to assume progress. Then we show that the implementation is branching bisimilar with the specification, and hence is also assumed to be correct / to satisfy this requirement. This method allows us to implicitly assume strong fairness. In fact we can even prove systems correct in cases where strong fairness is not strong enough. The form of fairness obtained in this way we call full fairness. Full fairness cannot be seen as a completeness criterion, because there are no specific paths that are ruled out. Yet it is a method to prove liveness properties, and on that basis it can be compared with strong fairness, and turns out to be strictly stronger.
In CTL, a useful liveness property often has the form
It is called an AGAF property, and says that whenever some precondition $\varphi$ is met, then eventually we reach a state where $\psi$ holds. By means of full fairness, we can obtain such a result, as soon as we have the weaker property
This AGEF property says that whenever some precondition $\varphi$ is met, it will always remain possible to reach a state where $\psi$ holds.
The notions of (rooted) branching (or weak) divergence-preserving bisimulation equivalence do not make fairness of justness assumptions.
We use the De Nicola-Vaandrager translation from process graphs to Kripke structures. Formally, a process graph is a triple (S,I,→), with S a set (of states), I∈S an initial state, and → a set of triples (s,a,t) with s,t ∈S and a an action, drawn from a set Act. The associated Kripke structure is $(S',I,\rightarrow',\models)$, where $S' := S \cup\{(s,a,t)\in{\rightarrow}\mid a\neq \tau\}$, and ${\rightarrow'} := \{(s,(s,a,t)),((s,a,t),t) \mid (s,a,t)\in S'\} \cup \{(s,t)\mid (s,\tau,t) \in {\rightarrow}\}$. This Kripke structure has the same states and transitions as the process graph, except that a new state $(s,a,t)$ is added halfway a transition from $s$ to $t$ labelled $a\neq\tau$. As atomic propositions we take the set Act of actions, except for $\tau$, and declare that a state satisfies the atomic proposition $a\in Act$ iff that state has the form $(s,a,t)$. So $r \models a$ iff $r=(s,a,t)$.
Now we consider all possible subsets $B$ of $Act\setminus\{\tau\}$. $B$ contains the actions that may be blocked by the environment. We define a $B$-complete path of a process graph as a path that is either infinite or ends in a state of which all outgoing transitions have a label from $B$. A $B$-complete path in a Kripke structure that arises as the De Nicola-Vaandrager translation of a process graph is a path that ends in a state, all of whose successor states are labelled with atomic propositions from $B$. Thus, the De Nicola-Vaandrager translation maps $B$-complete paths in process graphs to $B$-complete paths in the associated Kripke structures. An LTL formula $\phi$ is said to hold for the Kripke structure $K$ when the actions from $B$ might be blocking, notation $K \models_B \phi$, iff each $B$-complete path from the initial state of $K$ satisfies $\phi$. Likewise, $\models_B$ can be defined for CTL by simply replacing all references to infinite paths by $B$-complete paths.
As an example, consider a vending machine that takes in a coin $c$ and produces a pretzel $p$. We assume that taking in the coin requires cooperation from the environment, but producing the pretzel does not. A process algebraic specification is $$VM=c.p.VM$$ In old-fashioned LTL we have $VM \models G(c\Rightarrow Fp)$. This formula says that whenever a coin is inserted, eventually a pretzel is produced. This formula is intuitively true indeed. But we also have $VM \models G(p\Rightarrow Fc)$. This formula says that whenever a pretzel is produced, eventually a new coin will be inserted. This formula is intuitively false. This example shows that old-fashioned LTL is not suitable to describe the behaviour of this vending machine. Instead we use reactive LTL, and take $B=\{c\}$. This choice of $B$ says that the environment may bock the action $c$, namely by not inserting a coin; however, the environment may not block $p$. (Alternatively, one can interpret $B$ as an agreement with the user/environment, namely that the environment will never block actions outside of $B$.) As intuitively expected, we have $VM \models_B G(c\Rightarrow Fp)$ but $VM \not\models_B G(p\Rightarrow Fc)$.
Note that the old-fashioned LTL/CTL interpretation $\models$ is simply $\models_\emptyset$, obtained by taking the empty set of blocking actions.
There are 3 ways to incorporate the above idea.
Thus dealing with liveness properties under justness assumptions (without assuming weak fairness) calls for a semantic equivalence that distinguishes processes that are interleaving bisimilar. In fact, this opens a new dimension in our lattice of equivalences.
I review a few extensions of CCS-like languages in which it is possible to correctly model fair schedulers and mutual exclusion protocols. These come in two types:
In the second class one finds CCS, or labelled transition systems, extended with timeout actions.
Now a data expression is made from these constants and from variables ranging over a particular data type by applying the functions or operators specified by the data structure. For instance append(8+n,q) is a data expression of type queue. It is built from the constant 8 of type integer, the variable n of type integer, the binary operator + of type integer, the variable q of type queues of integers, and the operator append mentioned above.
Instead of atomic actions like a and b, we use actions that model the transmission of data over certain channels. In value-passing ACP there may be actions s_{c}(d) indicating the sending of data d over the channel c. In value-passing CCS, the action a(d) denotes the sending of data d on the channel c. Here c is taken from a set of channels names, where each channel comes with a certain data type, and d is a data expression of that type. The action c(x) represents the receipt of some data on some channel c. Here x is a variable of the data type required by c. The process (c(5).0 | c(x).b(x+2).0)\c) in value-passing CCS, for example, first communicates the value 5 over channel c: the left component sends 5 and the right-hand side receives it, binding it to the variable x. This communication takes the shape of a $\tau$-transitions, abstracting from the transmitted value. Then the right-hand component sends the value 5+2=7 on channel b.
The other two transition rules for parallel composition, and the rules for $+$, are exactly the same as for standard CCS. So are the rules for 0, restriction and renaming, noting that the data carried around by actions is not affected by restriction and renaming operators. The rule for recursion is $$ \frac{E \{\vec{exp}/\vec{x}\} \stackrel{\alpha}{\longrightarrow} Q}{X(\vec{exp}) \stackrel{\alpha}{\longrightarrow} Q}$$ when $X(\vec{x}) = E$ is the defining equation for the recursion constant $X$. The semantics for guards is more difficult, and skipped here, and we do not use assignment in this setting.
The rule for the send prefix now is $$(\xi, \bar{a}(\vec{exp}).P) \stackrel{\bar{a}(\xi(\vec{exp}))}{\longrightarrow} (\xi,P). $$ The difference with the previous semantics is that the vector of expressions $\vec{exp}$ is now converted through the valuation function $\xi$ into a vector of values. Thus the arguments of actions in transition labels have a semantic rather than a syntactic nature.
The rule for the read prefix becomes $$(\xi, a(\vec{x}).P ) \stackrel{a(\vec{v})}{\longrightarrow} (\xi[\vec{x}:=\vec{v}], P).$$ Here $\vec v$ may be any vector of values of the types of the variables $\vec x$. Thus, if we have $a(n).P$, with $n$ a variable for type integer, then there are infinitely many outgoing transitions, namely one for each integer that can be received when reading $x$ on channel $a$. The valuation $\xi[\vec{x}:=\vec{v}]$ is just $\xi$, but updated to now bind the values $\vec v$ to the variables $\vec x$.
In this approach the effort of passing values from a sending to a receiving process is shifted from the communication rule for parallel composition (see above) to the read and send prefixes. The rule for communication is simply $$\frac{(\xi,P) \stackrel{\bar c(\vec{v})}\longrightarrow (\zeta,P') \qquad (\xi,Q) \stackrel{c(\vec v)}\longrightarrow (\zeta,Q')}{(\xi,P | Q) \stackrel{\tau}\longrightarrow (\zeta,P'|Q')}$$ similar to standard CCS. A problem in applying this rule, is that at the sending end we normally have a transition $(\xi,Q) \stackrel{\bar c(\vec v)}\longrightarrow (\xi,Q')$ rather than $(\xi,Q) \stackrel{\bar c(\vec v)}\longrightarrow (\zeta,Q')$. This problem can be solved by postulating that $(\xi,Q')=(\zeta,Q')$ when $\xi(x)=\zeta(x)$ for all data variables $x$ that actually occur in $Q'$. By renaming the bound variables $\vec{x}$ within expressions $a(\vec{x}).P$ one can arrange for these variables not to occur within the parallel process $Q$, and this way the above agreement between $\xi$ and $\zeta$ can be reached.
The other two transition rules for parallel composition, and the rules for $+$, are again exactly the same as for standard CCS, and so are the rules for 0, restriction and renaming. The rule for recursion is $$ \frac{(\zeta,E) \stackrel{\alpha}{\longrightarrow} (\chi,Q)}{ (\xi,X(\vec{exp})) \stackrel{\alpha}{\longrightarrow} (\chi,Q)}$$ when $X(\vec{x}) = E$ is the defining equation for the recursion constant $X$. Here $\zeta$ is a valuation defined on the variables $\vec x$, such that $\zeta(\vec{x}) := \xi(\vec{exp})$.
The rule for guards is $$\frac{\xi(\varphi)={\bf true} \qquad (\xi,P) \stackrel{\alpha}{\longrightarrow} (\zeta,P')} { (\xi, [\varphi]P) \stackrel{\alpha}{\longrightarrow} (\zeta,P')}$$ and the rule of assignments $$ (\xi,[[ x:= exp ]]P) \stackrel{\tau}{\longrightarrow} (\xi[ x:= \xi(exp)], P).$$
The rule for send prefixing is $$ \bar{a}(\vec{exp}).P \stackrel{\bar{a}([[\vec{exp}]])}{\longrightarrow} P$$ where the operator $[[ ... ]]$ converts a closed data expression (or formula) into the data value it denotes; for instance $[[2+5]] = 7$ (or $[[7 > 5]] = \bf true$). The rules for read prefixing are $$ a(\vec{x}).P \stackrel{a(\vec{v})}{\longrightarrow} P\{\vec{v}/\vec{x}\}. $$ As above, $\vec v$ may be any vector of values of the types of the variables $\vec x$. The process expression $P\{\vec{v}/\vec{x}\}$ is the result of substituting (expressions denoting) the values $\vec v$ for the variables $\vec x$ in $P$. Note that since the variables $\vec x$ are bound in $a(\vec{x}).P$, this is a process without free variables, that is, a closed process expression. However, the expression $P$ may contain free occurrences of $\vec x$, and therefore does not count as a closed process expression. It is turned into a closed process expression by means of the substitution $\{\vec{v}/\vec{x}\}$. The rule for communication now is $$\frac{P \stackrel{\bar c(\vec{v})}\longrightarrow P' \qquad Q \stackrel{c(\vec v)}\longrightarrow Q'}{P | Q \stackrel{\tau}\longrightarrow P'|Q'}$$ and also the other two transition rules for parallel composition, and the rules for $+$, are exactly the same as for standard CCS. So are the rules for 0, restriction and renaming. The rule for recursion is $$ \frac{E \{\vec{exp}/\vec{x}\} \stackrel{\alpha}{\longrightarrow} Q}{X(\vec{exp}) \stackrel{\alpha}{\longrightarrow} Q}$$ when $X(\vec{x}) = E$ is the defining equation for the recursion constant $X$, just as in the late semantics. The rule for guards is $$\frac{[[\varphi]]={\bf true} \qquad P \stackrel{\alpha}{\longrightarrow} P'} { [\varphi]P \stackrel{\alpha}{\longrightarrow} P'}$$ and we do not use assignment in this setting.
Rob van Glabbeek | homework | rvg@cse.unsw.edu.au |