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 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 matched 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.
Here is the example of the relay race presented in class.
I also treated the optional extension ACP_{ε}, whose semantics is given by process graphs (or LTSs) in which not only end states but also intermediate states may be marked ✔.
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^{fin}(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 or just P =_{CT} 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 s. The set of all words accepted by s is the language accepted by s. 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 discussed 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 equivalence 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 graph 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 at the other hand are linear time equivalences, as they only focus on the linear executions of a process, without taking branching into account.
I also defined when one process simulates another. This is like bisimulation, but in the transfer property the initiative is always taken by the simulated process, and the matching move should be taken by the simulating process. Two processes are simulation equivalent if one simulates the other and vice versa. This is not the same as bisimulation equivalence, for there we insists on a single relation that is at the same time a simulation in both directions. The processes ab+a(b+c) and a(b+c) simulate each other, but are not bisimulation equivalent.
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}.
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. I presented the definition of weak bisimilarity in class.
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:
WPT^{fin} | |||
P | normal progress | a.b.0 | $\{ab,a,\epsilon\}$ |
Q | fair divergence | a.Δb.0 | $\{ab,a,\epsilon\}$ |
R | livelock | a.(b.0+ τ.Δ0) | $\{ab,a,\epsilon\}$ |
S | deadlock | a.(b.0 + τ.0) | $\{ab,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 were 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 b 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.
Branching bisimulation with explicit divergence ($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. Branching bisimulation equivalence with explicit divergence 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.
State s is internally divergent w.r.t. a colouring is 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 branching bisimulation equivalence with explicit divergence 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. I showed by a proof and a counterexample that this notion is strictly weaker than divergence preserving branching bisimilarity.)
Weak bisimilarity with explicit divergence ($WB^\Delta$) is defined much simpler: A weak bisimulation with explicit divergence 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 τ.
A state s is a deadlock state if it has no outgoing transitions.
A finite path π is a deadlock path if its last state is a deadlock state.
A state s is a livelock state if from s we can not reach
a deadlock state, nor a state from which a visible action can be performed.
A finite path π is a livelock path if its last state is a livelock state.
A state s is a divergence state if it is the beginning of an infinite path of τ-transitions.
A finite path π is a divergence path if its last state is a divergence state.
Let WCT^{δ}(G) := {wl(π) | π is a deadlock path of G}.
Let WCT^{λ}(G) := {wl(π) | π is a livelock path of G}.
Let WCT^{Δ}(G) := {wl(π) | π is a divergence of G}.
Note that WCT^{λ}(G) always is a subset of WCT^{Δ}(G).
These sets are illustrated on the examples given earlier:
WPT^{fin} | WCT^{δ} | WCT^{λ} | WCT^{Δ} | ||
normal progress | a.b.0 | $\{ab,a,\epsilon\}$ | $\{ab\}$ | $\emptyset$ | $\emptyset$ |
fair divergence | a.Δb.0 | $\{ab,a,\epsilon\}$ | $\{ab\}$ | $\emptyset$ | $\{a\}$ |
livelock | a.(b.0+ τ.Δ0) | $\{ab,a,\epsilon\}$ | $\{ab\}$ | $\{a\}$ | $\{a\}$ |
deadlock | a.(b.0 + τ.0) | $\{ab,a,\epsilon\}$ | $\{ab,a\}$ | $\emptyset$ | $\emptyset$ |
The question was: Modify the definition of weak completed trace semantics in six different ways, namely such that
Infinitary weak completed trace equivalence (WCT^{∞}) can be defined in the same way: two processes are infinitary weak completed trace equivalent if, after leaving out all occurrences of τ from their (possibly infinite) strong completed traces, their resulting sets of weak completed traced are the same. Here one should realise that we can obtain a finite weak complete trace by leaving out all occurrences of τ from an infinite strong complete trace. The most straightforward form of finitary weak completed trace equivalence (WCT^{fin}) is obtained by requiring that two process have the same set of weak traces obtained from leaving out τ's from finite strong complete traces—thereby skipping the finite traces obtained by leaving out all occurrences of τ from infinite strong complete traces—and moreover requiring that they have the same finite weak partial traces.
Surprisingly, WCT^{∞} is not finer than WCT^{fin}. This is shown in the following table: WCT^{fin} distinguishes deadlock from livelock, whereas WCT^{∞} does not.
WCT^{fin} | WCT^{∞} | WCT^{Δ} | WCT^{λ} | ||
normal progress | a.b.0 | $\{ab\}$ | $\{ab\}$ | $\{ab\}$ | $\{ab\}$ |
fair divergence | a.Δb.0 | $\{ab\}$ | $\{ab,a\}$ | $\{ab,a\Delta\}$ | $\{ab\}$ |
livelock | a.(b.0+ τ.Δ.0) | $\{ab\}$ | $\{ab,a\}$ | $\{ab,a\Delta\}$ | $\{ab,a\}$ |
deadlock | a.(b.0 + τ.0) | $\{ab,a\}$ | $\{ab,a\}$ | $\{ab,a\}$ | $\{ab,a\}$ |
None of the above equivalences would be suitable for a verification of the alternating bit protocol. For there fair divergence is the expected behaviour, and this should be distinguished from livelock, which is bad behaviour.
To arrive at a form of weak completed trace equivalence that distinguishes livelock from fair divergence, call a process q (or state) locked if q has no partial trace containing a non-τ action. A lock must be either a deadlock or a livelock. Now a deadlock/livelock-trace of a process p, is the sequence of visible actions on a path from q to a locked state q. Let WCT^{λ}(p) be the set of deadlock/livelock-trace of p. Two processes p and q are deadlock/livelock-preserving (finitary) completed trace equivalent, notation P =_{WCT}^{λ} Q, if WCT^{λ}(p) = WCT^{λ}(q) and also WPT^{fin}(p) = WPT^{fin}(q).
To distinguish all four phenomena, we can now define an equivalence =_{WCT}^{Δλ} by P =_{WCT}^{Δλ} Q iff WCT^{Δ}(p) = WCT^{Δ}(q) and WCT^{λ}(p) = WCT^{λ}(q).
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 $ab+ac$ and $a(b+c)$ are completed trace equivalent, but after placing them in a context $\partial_{\{b\}}(\_)$ or $\_\backslash b$ or $\_\|_{\{b\}}0$ they are not. 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 finer 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 (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 and expression is called a head normal form. 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.
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:
In fact, the same can be done for all other equivalences we encountered (such as weak and strong completed trace equivalence) and we indicated 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 RWB equivalent iff
RWB equivalence equals weak 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.
The congruence closure of branching bisimilarity can be obtained in a similar way: two processes are branching 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 branching bisimulation, one that relates initial states with initial states only. It turned out that two processes P and Q are RBB equivalent iff
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.
When using equational reasoning to verify that a specification is equivalent to an implementation we use, in addition to the machinery of equational logic, the recursive definition principle (RDP) and the recursive specification principle (RSP). RDP says that a system satisfies its recursive definition; RSP says that two processes satisfying the same guarded recursive equation, must be equal. It holds for strong and rooted weak or branching bisimilarity. These principles are applied in last week's handout on the verification of correctness of the alternating bit protocol.
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 this handout, and especially note how Definition 3 of bisimulation avoids having the clause on initial states.
Today I presented the theory of structural operational semantics, as described in this handout. (The handout, however, deals also with negative premises, which were not treated in class yet.) I also covered the structural operational semantics of CCS, given here. (Only read the first section.) What is called $\textbf{fix}_XS$ in the handout was called <X|S> in class. The rule for recursion involves substitution. (The operational rules for basic CCS are given in Example 1 of this handout. (In class I wrote P and Q for x_{1} and x_{2}, and P' for y_{1}.))
I also explained 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. We covered a 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.
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, negatation is not eleminated, but instead a variable needs to be under an even number of negation operators. This treatment is equivalent.
E ⊨ true | ||
E ⊭ false | ||
E ⊨ Φ∧Ψ | iff | E ⊨ Φ and E ⊨ Ψ |
E ⊨ Φ∨Ψ | iff | E ⊨ Φ or E ⊨ Ψ |
E ⊨ [K]Φ | iff | ∀F∈{E':E--a-->E' and a∈K} . F ⊨ Φ |
E ⊨ <K>Φ | iff | ∃F∈{E':E--a-->E' and a∈K} . F ⊨ Φ |
In the lecture I explained HML using a couple of different examples. I also showed how to model the concept of deadlock or termination in HML.
We then looked into properties of HML formulas and processes. In particular, we defined when two processes are indistinguishable.
To apply CTL or LTL to labelled transition systems we need a translation $\eta$ that maps (states in) labelled transition systems to (states in) Kripke structures. We then define validity of an LTL or CTL formula $\phi$ on a state $p$ in an LTL by $$p \models_\eta \phi \Leftrightarrow \eta(p) \models \phi$$ A suitable transition $\eta$ introduces a new state halfway each non-τ transition, and transfers the transition label to that state.
Two processes (states in a deadlock-free LTS) satisfy the same LTL formulas if they have the same infinite traces. For finitely-branching processes, we even have "iff".
Two processes (states in a deadlock-free LTS) satisfy the same LTL_{-X} formulas if they have the same weak infinite traces (obtained by leaving out τ's).
Two processes (states in a deadlock-free LTS) satisfy the same CTL formulas if they are 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 (states in a deadlock-free LTS) satisfy the same CTL_{-X} formulas if they are branching bisimilar with explicit divergence. We even have "iff", provided that we use CTL_{-X} with infinite conjunctions.
We also extended 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 branching bisimilar with explicit divergence. 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 branching bisimilarity with explicit divergence, which would identify deadlock and livelock.
Modulo strong, branching or weak bisimulation, every process graph can be converted into one in which no two states are bisimilar. The states of the canonical representation will be the bisimulation equivalence classes (colours) of the states of the original graph. The transitions between such states are defined in the obvious way, and the initial state is the equivalence class containing the initial state of the original system.
The handout uses equational reasoning (applying axioms and such) 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 this book.
Of course equivalence checking and model checking can be combined: there are theorems that tell is that if Spec ~ Impl for a suitable equivalence ~, and Spec satisfies a temporal formula of a particular form, then also Impl satisfies this formula.
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) equivalence seen before. We will soon encounter alternative forms of these equivalences that do not incorporate a fairness assumption. 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.
I indicated how causal trace semantics can be represented in terms of pomsets, partial ordered multisets. The process $a(b||(c+de)))$ for instance has two completed pomsets, which were drawn in class. A normal trace can be regarded as a totally ordered multiset of actions.
In this handout the definition of a labelled prime event structure with binary conflict can be found, as well as its translation into a process graph.
Here is a more thorough account of event structures. In class I told how operators of CCS and related languages can be interpreted in terms of event structures. This corresponds with Section 2.3 of that paper.
I also gave a Game theoretical characterisation of strong bisimilarity. The details are in wikipedia.
Finally, I introduced Petri nets, and gave an interpretation of the operators of CCS etc. in terms of nets. Thus also Petri nets can be used as semantic model of such languages.
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.
Afterwards I described the essence of safety properties, saying that something bad will never happen, and liveness properties, saying 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. We formulated these properties in LTL and CTL.
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. 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. Whether a "bad" outgoing transition occurs in a state also depends on the values of those variables, and the invariants we need says this never happens.
Whether liveness properties of systems hold depends often on whether or not we make appropriate progress and fairness assumptions. I discussed 4 such assumptions: progress, justness, weak fairness and strong fairness. Please read page 7 of this paper for an informal description of these properties.
When assuming justness but not weak fairness, there are two bisimilar systems with different liveness properties. Have a look at the section "Process algebras without fairness assumptions, and their limitations" in this paper.
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, to be revealed next week.
This examples deals with global fairness assumption. It is also possible to point at a Petri net (or some other system description) and mark certain choices as fair, and others as unfair; this gives local fairness assumptions. Due to lack of time we do not treat those here.
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) equivalence seen before. The notions of (rooted) branching (or weak) bisimulation equivalence with explicit divergence do not make fairness of justness assumptions. A progress assumption is build in in the logics CTL and LTL (for they work with infinite paths rather than partial paths).
My personal opinion is that it is often reasonable to assume (global) progress. In the absence of that, no non-trivial liveness property can be proven. When assuming progress I find it reasonable to also assume justness (globally). However, the use of global (weak or strong) fairness assumption should not be our default; it should be used only if for some reason we are convinced that such an assumption is warranted, or because we can only obtain a meaningful liveness property conditionally on making such an assumption.
After the break, Patrick Gilfillan presented Chu spaces.
In the last 10 minutes I presented "reactive CTL/LTL". A few weeks ago we say how to interpret CTL and LTL on process graphs (or states in labelled transition systems) with deadlocks. We discussed 3 methods to deal with deadlock. In the context of CTL or LTL minus the next-state operator, the 3rd method was the best. But when using full CTL or LTL, with the next-state operator, the 2nd method is just as good, and this is what I use today. In a deadlock state in a Kripke structure (a state without outgoing transitions), the CTL formula AXfalse holds, and in a state with an outgoing transition it does not hold. Hence this formula could be used to describe deadlock.
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=a.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$. 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.
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 a 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 structural operational semantics is the same as before, except that the rule for communication now is $$\frac{P \stackrel{\bar c(d)}\longrightarrow P' \qquad Q \stackrel{c(x)}\longrightarrow Q'}{P | Q \stackrel{\tau}\longrightarrow P'|Q'\{v/x\}}$$ Here $d$ denotes a data expression of the data type specified by the channel c and $Q'\{d/x\}$ denotes the process $Q$ with $d$ substituted for all free occurrences of the variable $x$. There are different ways in which this can be made more precise; due to lack of time I will not do this here.
Rob van Glabbeek | homework | rvg@cse.unsw.edu.au |