Equivalences and Preorders

4.3 Equivalences and Preorders

This section will describe a rather novel use of the modal µ-calculus as a meta-language for describing equivalences and preorders. The advantage of this approach is that having expressed an equivalence or a preorder as a formula in the logic, all the techniques and algorithms developed for the logic become directly applicable for that equivalence or preorder. We will see how familiar techniques of showing processes equivalent can be re-discovered as special cases of general techniques for theµ-calculus, and how new techniques emerges.

But first we consider some very familiar equivalences due to Milner [59].

Example 4.3 (Strong bisimilarity) (Milner [59, p.88ff]) Recall that two processes p and q are strongly bisimilar written p ∼ q, if and only if, (p, q) belongs to the maximum fixed-point of the function F onP(Sp×Sq) defined by (p, q)∈F(R)⇔def ∀a∈Act.

(i) ∀p. p→^a p ⇒ ∃q. q→^a q & (p, q)∈R (ii) ∀q. q →^a q ⇒ ∃p. p→^a p & (p, q)∈R Now, notice that F(R) can be expressed quite directly as

∀˜α.[α× ∗]∗ ×αR∧[∗ ×α]α× ∗R hence the µ-calculus version of ∼ becomes

B =def νR.∀˜α.[α× ∗]∗ ×αR∧[∗ ×α]α× ∗R Notice, that ad(B) = 1. ✷

It is now straightforward to prove:

Proposition 4.1 For processes p and q of type ·, p ∼ q, if and only if, p×q |=B.

Example 4.4 (Weak bisimilarity and observation congruence) Forweak bisimulation(also calledobservation equivalenceMilner [59, p.108ff]) we need to introduce the notion ofweak transitions capturing essentially what is ‘visible’ ignoring the ‘invisible/internal’ action τ. Following our previous discussion on regular expressions in example 4.1, we can simply define

⇒a = ^τ∗→^aτ∗, if a=τ

⇒τ = →^τ∗

Two processes p and q are weakly bisimilar written p ≈ q, if and only if, (p, q) belongs to the maximum fixed-point of the function F on P(Sp ×Sq) defined by (p, q)∈F(R)⇔def ∀a∈Act.

(i) ∀p· p→^a p ⇒ ∃q· q⇒^a q & (p, q)∈R (ii) ∀q · q →^a q ⇒ ∃p· p⇒^a p & (p, q)∈R

Now, to express this as an assertion we need to introduceweak modalities of type· × ·, two versions allowing the left respectively the right component to make a weak transition while the other idles. Following the lines of example 4.1, we first define two more general constructions allowing the left and right component to perform transitions of arbitrary regular expressions. Define for an assertionA of type · × ·, and R of type ·,RlA inductively as follows:

αlA = α× ∗A R0R1lA = R0l(R1lA) R0∪R1lA = R0lA∨ R1lA

R^∗lA = µX.RlX∨A, for some X /∈F V(A) and analogously for RrA with the first clause changed to

αrA=∗ ×αA.

We can now define a weak diamond left and weak diamond right modality:

αlA = τ^∗ατ^∗lA∨(α =τ ∧A) αrA = τ^∗ατ^∗rA∨(α =τ ∧A).

The first assertion is satisfied by a productp×q if p⇒^α p andp×q satisfies A. Using this we can express≈ as the assertion

W =def νR.∀α.[α˜ × ∗]αrR∧[∗ ×α]αlR Forobservation congruence (written ‘=’ Milner [59, p.153]) we take

C =def ∀˜α.[α× ∗]τ^∗ατ^∗rW ∧[∗ ×α]τ^∗ατ^∗lW

4.3 Equivalences and Preorders 93

Notice, that ad(W) =ad(C) = 2. ✷ It is again straightforward to show:

Proposition 4.2 For processes p and q, p ≈ q, if and only if, p×q |= W, and p=q,if and only if p×q|=C.

Example 4.5 (Ready simulation) (Bloom [13], Bloom and Paige [14]) A state p is said to ready simulate a state q if (p, q) belongs to the maximal fixed-point of the function F on Sp×Sq defined by (p, q)∈F(R)⇔def

(i) ∀a ∈Act. ∀p. p→^a p ⇒ ∃q. q→^a q & (p, q)∈R (ii) ∀a ∈Act. p→ ⇔^a q→^a.

This is captured by the assertion

R =νR.∀α.[α× ∗]∗ ×αR∧(α× ∗T ↔ ∗ ×αT).

Ready bisimulation (also called 2/3-bisimulation) is simply the conjunction of R and its reverse R⁻¹ defined by transforming α× ∗(respectively ∗ ×α) to ∗ ×α (respectivelyα× ∗) in the definition ofR. Hence RB =R ∧ R⁻¹.

Notice that ad(RB) = ad(R) = 1. ✷ Example 4.6 (Simulation preorder)

As an example of a preorder we consider thesimulation relation≺defined by Milner [59, p.208], as the maximum fixed-point of the functionF onP(S×S) defined by (p, q)∈F(R)⇔def

∀a∈Act. ∀p. p⇒^a p ⇒ ∃q. q ⇒^a q & (p, q)∈R Take

S =def νR.∀α[[α]]˜ lαrR.

Once again we can easily show p ≺ q if and only if p×q |= S and observe that ad(S) = 2. ✷

Example 4.7 (Prebisimulation)

To take proper care of the possible divergent behaviour of processes coming

from for instance infinite ‘internal chatter’ manifesting itself as an infinite sequence of silent actions, transition systems with a divergence predicate has been studied, and a preorder called prebisimulation defined. This can also be expressed within the modalµ-calculus as an assertion. First, a transition system with divergence is a tuple (S, i, L,→,↑) where (S, i, L,→) is a normal transition system and ↑⊆ S is a subset of divergent states. The divergence set ↑ is often thought of as a predicate using s ↑ for s ∈↑. We denote the complement of ↑ by↓, i.e. ↓=S\ ↑.

To express this in the logic we assume the presence of a constant Conv with valuationV(Conv) =↓, and constantsConv×T and T ×Conv of type

· × ·with valuations V(Conv×T) =↓ ×S and V(T ×Conv) =S× ↓. Now, the prebisimulation preorder 1 is the greatest fixed-point of the function F onP(S×S) defined by (p, q)∈F(R)⇔def ∀a∈Act.

(i) ∀p. p→^a p ⇒ ∃q. q →^a q & (p, q)∈R

(ii) p↓⇒q ↓& (∀q. q→^a q ⇔ ∃p. p→^a p & (p, q)∈R).

(Note that if↓=S then this definition degenerates to the usual definition of bisimulation.) In the logic this becomes

νR.˜∀α.[α× ∗]∗ ×αR∧((Conv×T)→((T ×Conv)∧[∗ ×α]α× ∗R)) with ad = 1. Again it is very easy to construct a weak version of this with ad= 2.² ✷

Example 4.8 (Characteristic formulae)

Through the product reduction, we can achieve characteristic formulae with respect to any equivalence, or preorder described as aµ-calculus formula. As an example, we consider the simple buffer

defined by

2The divergence predicate is sometimes chosen to be the set of states that might perform an infinite sequence of τ’s. This could be expressed internally in the logic as τ^ωT = νX.τX.

4.3 Equivalences and Preorders 95 P = in?P

P = out!P

and find a formula which is satisfied precisely by processes which are strongly bisimilar to the buffer: by distributing ˜∀ over the conjunctions.

For weak bisimulation we first observe that for all s (αlA/s=α(A/s),

(As a sideremark we notice that a has the following property:

|=s :aA⇔ ∃s. s⇒^a s &|=s :A.

Hence the logic is also adequate for ⇒^a.)

Returning to our example we observe that

(αrA)/P = (α =in?)∧(A/P), and

(αrA)/P = (α =out!)∧(A/P).

Temporal properties - and temporal logics - are normally classified as relat-ing to linear time or branching time dependent upon whether they express properties about paths of transitions (often also called runs) or trees of tran-sitions. Arguments exists for and against both views, as well as arguments for coexistence of the views (see f.ex. Lamport [52] and Emerson and Halpern [36]). We take the rather pragmatic approach that both classes are useful, and show how some of each class are expressible within the logic. At first sight, the modalµ-calculus is very much a branching time logic. The seman-tics is in terms of transition systems, which can be thought of as compact representations of trees of transitions, and the modalitiesαand [α] exploits the branching structure of the underlying models by quantifying over ‘vari-ous future states’. However, as the translations from other logics – including logics with linear time features – shows, it is possible to mimic the linear time aspect.

4.4.1 A Linear Time Logic

The modal µ-calculus is classified as a branching time logic referring to the property that the modalitiesa and [a] quantify over possible futures. Nev-ertheless, expressivity results show that alsolinear time logics referring in a certain sense to only one possible future, can be embedded into the modal µ-calculus ([49, 79, 30]). We will consider a very succinct embedding of a simple logic combining linear and branching time features, which apart from the usefulness of the translation will supply us with a collection of derived operators (or ‘macros’).