M =send?(rec!M+τ) +ackr?acks!M
Hence, after having received a message, M can decide to break down. The system is now
Sys = (SM R)A
where for convenience we simple restrict the visible behaviour to the neutral actions A. Now, alternatively we could assume that the medium could get into a state where instead of breaking down it will be occupied with internal
“chatter” and prevent itself from ever delivering the message. This could be modelled by the medium M:
M = send?(rec!M+τ L) +ackr?acks!M L = τ L
and the system
Sys = (S M R)A
Are these systems deadlock-free? Or formulated as correctness asser-tions, do we have Sys : DeadLockFree, Sys : DeadLockFree, Sys : Dead-LockFree where V(WellTerm) = {p | W(p)} from figure 2.10? We leave it to the reader to verify that the transition systems for Sys (which has four states) and for Sys and Sys (which has five states) are as shown in figure 2.11, and compute [[DeadLockFree]], for Sys, Sys and Sys, to find out that indeed
|=Sys : DeadLockFree, |= Sys : DeadLockFree but
|= Sys : DeadLockFree.
✷
2.6 Alternation Depth
Crucial for the expressive power of the modalµ-calculus is the ability to nest minimum and maximum fixed-points in a trivial manner, where by non-trivial we mean for instance a situation where if the outermost fixed-point
Figure 2.11: Transition systems pointed by Sys, Sys’, and Sys”.
operator is µ and some inner ν-fixed-point assertions contain free variables bound by theµ. The level of non-trivial nesting in an assertion is a somewhat tricky notion to capture and we have chosen to give the definition of this measure of alternation depth in an ‘operational’ fashion since the original motivation of defining it was to capture the complexity of a model-checking algorithm and the operational flavour fits well with our later complexity analyses.
But before applying the measure we assume that the assertions are transformed into positive normal form by pushing negations ‘inwards’ such that the assertion is built entirely from F, T,∧,∨,a,[a], X, µ, and ν (and Q,¬Q,∃α,∀α,γ,[γ],whereµ,and whereν for the alternation depth):
Proposition 2.3 Any assertion A in the standard (respectively extended) calculus has a logical equivalent A in the standard (respectively extended) calculus which is in positive normal form.
Proof: Easy. ✷
We first define the notion of alternation depth for the alternation depth for the standard calculus.
2.6.1 The Standard Calculus
We call an assertion with top-most operatorµ(respectivelyν)aµ-assertion (respectivelya ν-assertion).
Definition 2.9 For a closed assertion A, let cps(A) be the set of closed,
2.6 Alternation Depth 39 proper, µ- and ν-subassertions of A. Let mcps(A) ⊆ cps(A) be the set of maximal such assertions, i.e. assertions in cps(A) that are not subassertions of other assertions in cps(A). Moreover, let the top-level µ-subassertions, tlµ(A), of a closed assertionsA, be defined by structure induction as follows:
tlµ(F) = tlµ(T) = ∅
tlµ(A0∧A1) =tlµ(A0∨A1) = tlµ(A0)∪tlµ(A1) tlµ(aA) =tlµ([a]A) = tlµ(A)
tlµ(µX.A) = {µX.A} tlµ(νX.A) = tlµ(A[F/X]).
The function tlν is defined dually. ✷
We have chosen to replace, somewhat arbitrarily, F for X in the body of the maximum fixed-point to keep assertions closed.
Definition 2.10 The alternation depth ad(A) of a closed assertion A, is defined by induction on A as follows (we take max∅= 0):
The purpose of the measure ad is to capture to what extent minimum and maximum fixed-points are nested in an essential way. Hence, closed as-sertions appearing inside µ- and ν-assertions do not increase the alternation depth, nor does sequences of fixed-points of the same kind, only when for instance a ν-assertion appears inside some µ-assertion with a free variable bound by the µ-assertion, will the alternation depth increase.
Example 2.2 Some simple examples:
ad(aT ∨[b]F) = 0 ad(µX.νY.X∧ aY) = 2 ad(µX.X∧νY.aY) = 1
ad(νX.µY.νZ.[a]X∧(Y ∨Z)) = 3 ad(µY.(νZ.[a]F ∨ bZ)∨[c]Y) = 1 ad(νX.µY.(νZ.[a]X∨ bZ)∨[c]Y) = 2
✷
Remark 2.3 The notion of alternation depth was introduced by Emerson and Lei [35]. However, their definition contains a minor error, and our no-tion is slightly stronger in the sense that we attach a lower measure to some assertions.
Consider for a moment the assertion µX.νY.X∧Y with ad(µX.νY.X ∧Y) = 2.
Although the examples of Emerson and Lei correctly suggests that their measure yields two in this particular case their definition wrongly yields one, because they require ‘top-level formulae’ to be proper subexpressions of the bodies of fixed-points [35, p.270] hence they consider only proper ν-subformulae of νY.X ∧Y in case AD9 [35, p.271] of which there are none -it is a minor error: eliminating the word ‘proper’ corrects -it.
There is a more subtle difference in the case of higher alternation depths.
An example is
µX.A(X, νZ.B(Z, µU.C(U, νY.D(Y, X)))) (2.4) whereA, B, C, andDcontain no fixed-points, and the notationA(X, νZ. . . .) indicates that the only free variables of A are X and the free variables of νZ. . . .. The Emerson and Lei measure yields 4, whereas the measure intro-duced here yields 2. The reason is that in our measure we consider X to be a constant inside the body of the outermost minimum fixed-point, hence the alternation depth is one plus the alternation depth of
νZ.B(Z, µU.C(U, νY.D(Y, F))). (2.5) Now, νY.D(Y, F) is a constant expression and so is µU.C(U, νY.D(Y, F)) hence the alternation depth of (2.5) is one, and the alternation depth of (2.4) is two.
2.6 Alternation Depth 41 We believe that this was the definition originally intended by Emerson and Lei since it correctly captures the complexity of their algorithm, which is not the case with their definition – it is too pessimistic. In this last respect our definition also differs from that of Bradfield’s [15, p.23].
We return to the relationshipbetween complexities of model checking algorithms and alternation depth in chapter 5. ✷
2.6.2 The Extended Calculus
In order to generalize the definition of alternation depth to the extended calculus we must generalize mcps and tlµ. First, the notion of a µ-assertion is extended toµKextin the obvious way by considering an assertion with top-most operatorwhereµ to be a µ-assertion and dually for aν-assertion. Now, mcps(A) is again the set of maximal, closed, proper µ- and ν-subassertions of A. The functiontlµ (and dually tlν) is extended by
If mcps(A) =∅ then the defining clauses for ad is extended to products by:
ad((A1, . . . , An)) = max{ad(A1), . . . , ad(An)}
and for the constants, action predicates and quantifiers the extension is triv-ial.