5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 54
Текст из файла (страница 54)
A randomized arbiter,see the program graphs in Figure 5.9, decides which process is acquiring access to thecritical section. It does so by tossing coins. We abstract from the probabilities, andmodel the coin tossing by a nondeterministic choice between the alternatives “heads” and“tails”.
It is assumed that the two contending processes communicate with the arbitervia the actions enter1 and enter2 . The critical section is released by synchronizing over260Linear Temporal Logicnoncrit1noncrit2unlockreq1relreq2wait1enter1crit1relenter1relwait2tailsheadsenter2lockenter2crit2Figure 5.9: Mutual exclusion with a randomized arbiter.the action release. For the sake of simplicity, we refrain from indicating which process isreleasing the critical section.The property “process P1 is in its critical section infinitely often” cannot be established,since, for instance, the underlying transition system representation does not exclude anexecution in which only the second process may perform an action while P1 is entirelyignored.
Thus:TS1 Arbiter TS2 |= ♦ crit1 .If a coin is assumed to be fair enough such that both events “heads” and “tails” occur withpositive probability, the unrealistic case of one of the two alternatives never happeningcan be ignored by means of the unconditional LTL fairness assumption:fair = ♦heads ∧ ♦tails.It is not difficult to check that now:TS1 Arbiter TS2 |=fair ♦crit1 ∧ ♦crit2 .Example 5.28.Communication Protocol (Fairness)Consider the alternating bit protocol as described in Example 2.32 (page 57). For the sakeof convenience, the program graph of the sender of the alternating bit protocol is repeatedin Figure 5.10. The liveness property ♦start states that the protocol returns infinitelyoften to its initial state.
In this initial state the action snd msg(0) is enabled. It followsthatABP |= ♦startLinear Temporal Logic261c!m, 0snd msg(0)d?xst tmr(0)tmr onwait(0)lostchk ack(0)x=1timeoutx=1:tmr offx=0:tmr offtimeoutx=0chk ack(1)lostwait(1)tmr onst tmr(1)d?xsnd msg(1)c!m, 1Figure 5.10: Program graph of ABP sender S.since the unrealistic scenario in which (after some finite time) each message with alternating bit 1 is lost cannot be excluded. This corresponds to the pathlosttmr ontimeoutlost−→ si+1 −−−−−→ si+2 −−−−−→ si+3 −−−→ . . . . . .. . . .
. . si −−Suppose we impose the strong LTL fairness assumption(♦ (send (b) ∧ |c| = k) → ♦ |c| = k + 1).sfair =b=0,1kk<cap(c)Here, |c| = n stands for the atomic proposition that holds in the states , η, ξ in whichchannel c contains exactly n elements, i.e., the length of the word ξ(c) equals n. Thus,sfair describes (from the state-based point of view) that the loss of a transmitted messageis not continuously possible. We now obtainABP |=sfair ♦start.Note that it is essential to impose a strong fairness assumption on send(b); as this actionis not continuously enabled, a weak fairness assumption is insufficient.In Section 3.5 (page 126 ff.), fairness was introduced using sets of actions; e.g., an executionis unconditionally A-fair for a set of actions A, whenever each action α ∈ A occurs infinitelyoften.
LTL-fairness, however, is defined on atomic propositions, i.e., from a state-basedperspective. Is there any relationship between these two—at first sight, rather different—approaches toward fairness?The advantage of the action-based formulation of fairness assumptions is that many useful (and realizable) fairness assumptions can easily be expressed. Using the state-based262Linear Temporal Logicperspective, this may be less intuitive. For instance, the enabling of a process (or, moregenerally, of a certain action) is not necessarily a property that can be determined fromthe (atomic propositions in a) state.
This discrepancy is, however, not always present.n1 , n2 , y=1req2relreq1relw1 , n2 , y=1n1 , w2 , y=1req2enter2req1enter1c1 , n2 , y=0req2relw1 , w2 , y=1reln1 , c2 , y=0enter2req1enter1c1 , w2 , y=0w1 , c2 , y=0Figure 5.11: Semaphore-based mutual exclusion algorithm.Example 5.29.State-Based vs. Action-Based FairnessTo exemplify this, consider the semaphore-based two-process mutual exclusion protocol(see Figure 5.11) together with the action-based strong-fairness assumptionFstrong = { { enter1 }, { enter2 } }.Let us try to state the same constraint by means of a (state-based) LTL fairness assumption. Observe first that the action enter1 is executable if and only if process P1 is in thelocal state wait1 and process P2 is not in its critical section. Besides, on executing actionenter1 , process P1 moves to its critical section.
Thus, strong fairness for { enter1 } can bedescribed by the LTL fairness assumption:sfair 1 = ♦(wait1 ∧ ¬crit2 ) → ♦crit1 .The assumption sfair 2 is defined analogously. It now follows that sfair = sfair 1 ∧ sfair 2describes Fstrong .Fstrong requires each process to enter its critical section infinitely often when it infinitelyoften gets the opportunity to do so. This does not forbid a process to never leave itsnoncritical section.
To avoid this unrealistic scenario, the weak fairness constraintFweak = {{ req1 }, { req2 }}Linear Temporal Logic263requires that any process infinitely often requests to enter the critical section when it continuously is able to do so. This (action-based) weak fairness constraint can be formulatedas (state-based) LTL fairness assumption in a similar way as above. Observe that therequest action of Pi is executable if and only if process Pi is in the local state noncriti .Weak fairness for { reqi } thus correponds to the LTL fairness assumption:wfair i = ♦noncriti → ♦waiti .Let fair = sfair ∧ wfair where wfair = wfair 1 ∧ wfair 2 .
It then follows thatTSSem |=fair ♦crit1 ∧ ♦crit2 .In many cases, it is possible to replace action-based fairness by state-based LTL fairnessassumptions. This, however, requires the possibility to deduce from the state label thepossible enabled actions and the last executed action. It turns out that action-basedfairness assumptions can always be “translated” into analogous LTL fairness assumptions.This works as follows. The intuition is to make a copy of each noninitial state s such thatit is recorded which action was executed to enter state s.
Such copy is made for everypossible action via which the state can be entered. The copied state s, α indicates thatstate s has been reached by performing α as last action.Formally, this works as follows. For transition system TS = (S, Act, →, I, AP, L) letTS = (S , Act , → , I , AP , L )where Act = Act { begin }, I = I × { begin } and S = I ∪ (S × Act).
The transitionrelation in TS is defined by the rules:α→ ss −−α s, β −−→ s , αandαs0 −−→ s s0 ∈ Iα s0 , begin −−→ s, αThe state labeling is defined as follows. LetAP = AP ∪ { enabled(α), taken(α) | α ∈ Act }with the labeling functionL (s, α) = L(s) ∪ { taken(α) } ∪ { enabled(β) | β ∈ Act(s) }for s, α ∈ S × Act andL (s0 , begin) = L(s0 ) ∪ {enabled(β) | β ∈ Act(s0 ) }.264Linear Temporal LogicIt can easily be established thatTracesAP (TS) = TracesAP (TS ).Strong fairness for a set of actions A ⊆ Act can now be described by the strong LTLfairness assumption:sfair A = ♦enabled(A) → ♦taken(A)whereenabled(A) ="enabled(α)andtaken(A) =α∈A"taken(α).α∈AUnconditional and weak action-based fairness assumptions for TS can be transformed intoLTL fairness assumptions for TS in a similar way. For action-based fairness assumptionF for TS and fair the corresponding LTL fairness assumption for TS , it follows that theset of fair traces coincides:{traceAP (π) | π ∈ Paths(TS), π is F-fair}= {traceAP (π ) | π ∈ Paths(TS ), π |= fair }.Stated differently, FairTracesF (TS) = FairTracesfair (TS ) where in TS only atomic propositions in AP are considered.
In particular, for every LT property P over AP,TS |=F P iff TS |=fair P.Conversely, a (state-based) LTL fairness assumption cannot always be represented asaction-based fairness assumption. This fact follows from the fact that strong or weakLTL fairness assumptions need not be realizable, while any action-based strong or weakfairness assumptions can be realized by a scheduler. In this sense, state-based LTL fairnessassumptions are more general than action-based fairness assumptions.The following theorem shows that the satisfaction relation |=fair as defined in Definition 5.26 has a strong relation to the usual satisfaction relation |=.Theorem 5.30.Reduction of |=fair to |=For transition system TS without terminal states, LTL formula ϕ, and LTL fairness assumption fair :if and only ifTS |= (fair → ϕ).TS |=fair ϕLinear Temporal Logic265Proof: ⇒: Assume TS |=fair ϕ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
