5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 50
Текст из файла (страница 50)
For instance, the lengthof the formula true and a ∈ AP is 0. Formulae a ∨ b and a ∨ ¬b have length 2, and( a) U (a ∧ ¬b) has length 4. Throughout this monograph, mostly the asymptotic sizeΘ(| ϕ |) is needed. For this purpose, it is irrelevant whether or not the derived Booleanoperators ∨, →, and so on, and the derived temporal modalities ♦ and are taken intoaccount in determining the length.5.1.2SemanticsLTL formulae stand for properties of paths (or in fact their trace).
This means that apath can either fulfill an LTL-formula or not. To precisely formulate when a path satisfiesan LTL formula, we proceed as follows. First, the semantics of LTL formula ϕ is definedas a language Words(ϕ) that contains all infinite words over the alphabet 2AP that satisfyϕ. That is, to every LTL formula a single LT property is associated.
Then, the semanticsis extended to an interpretation over paths and states of a transition system.Definition 5.6.Semantics of LTL (Interpretation over Words)Let ϕ be an LTL formula over AP. The LT property induced by ϕ isWords(ϕ) = σ ∈ (2AP )ω | σ |= ϕwhere the satisfaction relation |= ⊆properties in Figure 5.2.(2AP )ω × LTL is the smallest relation with theHere, for σ = A0 A1 A2 . .
. ∈ (2AP )ω , σ[j . . .] = Aj Aj+1 Aj+2 . . . is the suffix of σ startingin the (j+1)st symbol Aj .Note that in the definition of the semantics of LTL-formulae the word fragment σ[j . . .]cannot be replaced with Aj . For the formula (a U b), e.g., the suffix A1 A2 A3 . . . has to236Linear Temporal Logicσ |= trueσ |= aiff a ∈ A0(i.e., A0 |= a)σ |= ϕ1 ∧ ϕ2 iff σ |= ϕ1 and σ |= ϕ2σ |=¬ϕσ |= ϕiff σ |= ϕiff σ[1 . . .] = A1 A2 A3 . . . |= ϕσ |= ϕ1 U ϕ2 iff ∃j 0. σ[j . . .] |= ϕ2 and σ[i . . .] |= ϕ1 , for all 0 i < jFigure 5.2: LTL semantics (satisfaction relation |=) for infinite words over 2AP .be regarded in order to be able to refer to the truth-value of the subformula a U b in the“next step”.For the derived operators ♦ and the expected result is:σ |= ♦ϕiff ∃j 0.
σ[j . . .] |= ϕσ |= ϕ iff ∀j 0. σ[j . . .] |= ϕ.The statement for ♦ is immediate from the definition of ♦ and the semantics of U . Thestatement for follows from:σ |= ϕ = ¬♦¬ϕiffiffiff¬∃j 0. σ[j . . .] |= ¬ϕ¬∃j 0. σ[j . . .] |= ϕ∀j 0. σ[j . . .] |= ϕ.The semantics of the combinations of and ♦ can now be derived:σ |= ♦ϕ iffσ |= ♦ϕ iff∞∃ j. σ[j . . .] |= ϕ∞∀ j. σ[j . . .] |= ϕ.∞∞Here, ∃ j means ∀i 0. ∃j i, “for infinitely many j ∈ IN”, while ∀ j stands for∃i 0. ∀j i, “for almost all j ∈ IN”.
Let us verify the first statement. The argumentfor the second statement is similar.σ |= ♦ϕiffiff∀i 0. σ[i . . .] |= ♦ϕ∀i 0. ∃j i. σ[j . . .] |= ϕiff∃ j. σ[j . . .] |= ϕ.∞As a subsequent step, we determine the semantics of LTL-formulae with respect to aLinear Temporal Logic237transition system. According to the satisfaction relation for LT properties (see Definition3.11 on page 100), the LTL formula ϕ holds in state s if all paths starting in s satisfy ϕ.The transition system TS satisfies ϕ if TS satisfies the LT property Words(ϕ), i.e., if allinitial paths of TS—paths starting in an initial state s0 ∈ I—satisfy ϕ.Recall that we may assume without loss of generality that transition system TS has noterminal states (if it has such states, a trap state can be introduced.
Thus, we may assumethat all paths and traces are infinite. This assumption is made for the sake of simplicity; itis also possible to define the semantics of LTL for finite paths. Note that for the semanticsit is irrelevant whether or not TS is finite. Only for the model-checking algorithm lateron in this chapter, is the finiteness of TS required.As for the LT properties, when defining TS |= ϕ for transition system TS over AP , itis assumed that ϕ is an LTL-formula with atomic propositions in AP = AP . (Here, onecould be more liberal and allow for AP ⊆ AP .)Definition 5.7.Semantics of LTL over Paths and StatesLet TS = (S, Act, →, I, AP, L) be a transition system without terminal states, and let ϕbe an LTL-formula over AP.• For infinite path fragment π of TS, the satisfaction relation is defined byπ |= ϕifftrace(π) |= ϕ.• For state s ∈ S, the satisfaction relation |= is defined bys |= ϕiff(∀π ∈ Paths(s).
π |= ϕ).• TS satisfies ϕ, denoted TS |= ϕ, if Traces(TS) ⊆ Words(ϕ).From this definition, it immediately follows thatTS |= ϕiff(* Definition 5.7 *)Traces(TS) ⊆ Words(ϕ)iffTS |= Words(ϕ)iff(* Definition of |= for LT properties *)(* Definition of Words(ϕ) *)π |= ϕ for all π ∈ Paths(TS)iffs0 |= ϕ for all s0 ∈ I.(* Definition 5.7 of |= for states *)238Linear Temporal LogicThus, TS |= ϕ if and only if s0 |= ϕ for all initial states s0 of TS.s1s2s3{ a, b }{ a, b }{a}Figure 5.3: Example for semantics of LTL.Example 5.8.Semantics of LTLConsider the transition system TS depicted in Figure 5.3 with the set of propositionsAP = { a, b }.
For example, we have that TS |= a, since all states are labeled with a,and hence, all traces of TS are words of the form A0 A1 A2 . . . with a ∈ Ai for all i 0.Thus, si |= a for i = 1, 2, 3. Moreover:s1 |= (a ∧ b) since s2 |= a ∧ b and s2 is the only successor of s1s2 |= (a ∧ b) and s3 |= (a ∧ b) as s3 ∈ Post(s2 ), s3 ∈ Post(s3 ) and s3 |= a ∧ b.This yields TS |= (a ∧ b) as s3 is an initial state for which s3 |= (a ∧ b). As anotherexample:TS |= (¬b → (a ∧ ¬b)),since s3 is the only ¬b state, s3 cannot be left anymore, and a ∧ ¬b in s3 is true. However,TS |= b U (a ∧ ¬b),since the initial path (s1 s2 )ω does not visit a state for which a ∧ ¬b holds. Note that theinitial path (s1 s2 )∗ sω3 satisfies b U (a ∧ ¬b).Remark 5.9.Semantics of NegationFor paths, it holds π |= ϕ if and only if π |= ¬ϕ.
This is due to the fact thatWords(¬ϕ) = (2AP )ω \ Words(ϕ).However, the statements TS |= ϕ and TS |= ¬ϕ are not equivalent in general. Instead, wehave TS |= ¬ϕ implies TS |= ϕ. Note thatTS |= ϕiff Traces(TS) ⊆ Words(ϕ)iff Traces(TS) \ Words(ϕ) = ∅iff Traces(TS) ∩ Words(¬ϕ) = ∅.Linear Temporal Logic239Thus, it is possible that a transition system (or a state) satisfies neither ϕ nor ¬ϕ. Thisis caused by the fact that there might be paths π1 and π2 in TS such that π1 |= ϕ andπ2 |= ¬ϕ (and therefore π2 |= ϕ).
In this case, TS |= ϕ and TS |= ¬ϕ holds.To illustrate this effect, consider the transition system depicted in Figure 5.4. Let AP ={ a }. It follows that TS |= ♦a, since the initial path s0 (s2 )ω |= ♦a. On the other hand,TS |= ¬♦a also holds, since the initial path s0 (s1 )ω |= ♦a, and thus, s0 (s1 )ω |= ¬♦a.s1s0s2{a}∅∅Figure 5.4: A transition system for which TS |= ♦a and TS |= ¬♦a.5.1.3Specifying Propertiesn1 , n2 , y=1w1 , n2 , y=1c1 , n2 , y=0n1 , w2 , y=1w1 , w2 , y=1c1 , w2 , y=0n1 , c2 , y=0w1 , c2 , y=0Figure 5.5: Transition system of semaphore-based mutual exclusion algorithm.Example 5.10.Semaphore-Based Mutual Exclusion RevisitedConsider the transition system TSSem depicted in Figure 5.5 which represents a semaphorebased solution to the mutual exclusion problem; see also Example 3.9 on page 98.
Each240Linear Temporal Logicstate of the form c1 , ·, · is labeled with proposition crit1 and each state of the form ·, c2 , ·is labeled with crit2 . It follows thatTSSem |= ( ¬ crit1 ∨ ¬ crit2 )and TSSem |= ♦crit1 ∨ ♦crit2 ,where the first LTL-formula stands for the mutual exclusion property and the secondLTL-formula for the fact that at least one of the two processes enters its critical sectioninfinitely often. However,TSSem |= ♦crit1 ∧ ♦crit2 ,since—in the absence of any fairness assumption—it is not ensured that process P1 isenabled infinitely often.
It may not be able to acquire access to its critical section once.(A similar argument applies to process P2 .) The same argument applies to show thatTSSem |= ♦wait1 → ♦crit1as in principle process P1 may not get its turn once it starts to wait.Example 5.11.Modulo 4 CounterA modulo 4 counter can be represented by a sequential circuit C, which outputs 1 inevery fourth cycle, otherwise 0. C has no input bits, one output bit y, and two registersr1 and r2 . The register evaluation [r1 = c1 , r2 = c2 ] can be identified with the numberi = 2 · r1 + r2 .
In every cycle, the value of i is increased by 1 (modulo 4). We constructC in a way such that the output bit y is set exactly for i = 0 (hence, r1 = r2 = 0). Thetransition relation and output function are given byδr1 = r1 ⊕ r2 , δr2 = ¬r1 , λy = ¬r1 ∧ ¬r2 .Figure 5.6 illustrates the diagram (on the left) and the transition system TSC (on theright). Let AP = { r1 , r2 , y }. The following statement can be directly inferred from TSC :TSC|= ( y ↔ ¬r1 ∧ ¬r2 )TSC|= ( r1 → ( y ∨ y) )TSC|= ( y → ( ¬y ∧ ¬y) )If it is assumed that only the output variable y (and not the register evaluations) can beperceived by an observer, then an appropriate choice for AP is AP = { y }.
The propertythat at least during every four cycles the output 1 is obtained holds for TSC , i.e., we haveTSC |= ( y ∨ y ∨ y ∨ y ).Linear Temporal Logic241NOTr1ANDyy00011110r2XORr1 r2r1NOTr2Figure 5.6: A modulo 4 counter.The fact that these outputs are produced in a periodic manner where every fourth cycleyields the output 1 is expressed asTSC |= ( y −→ ( ¬y ∧ ¬y ∧ ¬y) ).Example 5.12.A Communication ChannelConsider an unidirectional channel between two communicating processes, a sender S anda receiver R. Sender S is equipped with an output buffer S.out and recipient R with aninput buffer R.in. If sender S sends a message m to R it inserts the message into itsoutput buffer S.out. The output buffer S.out and the input buffer R.in are connected viaan unidirectional channel.
The receiver R receives messages by deleting messages from itsinput buffer R.in. The capacity of the buffers is not of importance here.A schematic view of the system under consideration is:Sender SS.outchannelR.inReceiver RIn the following LTL-specifications, we use the atoms “m ∈ S.out” and “m ∈ R.in” wherem is an arbitrary message. We formalize the following informal requirements by LTLformulae:• “Whenever message m is in the out-buffer of S, then m will eventually be consumedby the receiver.”(m ∈ S.out −→ ♦(m ∈ R.in))242Linear Temporal LogicThe above property is still satisfied for paths s1 s2 s3 .
. . where s1 |= m ∈ S.out,/ S.out, s2 |= m ∈/ R.in, and s3 |= m ∈ R.in. However, such paths stands2 |= m ∈for a mysterious behavior where message m in the output buffer for S (state s1 )gets lost (state s2 ), but still arrives in the input buffer of R (state s3 ). In fact, sucha behavior is impossible for a reliable FIFO channel which satisfies the followingstronger condition(m ∈ S.out −→ (m ∈ S.out U m ∈ R.in))stating that message m stays in S.out until the receiver R consumes m. Since writingand reading in a FIFO channel cannot happen at the same moment, we can evenuse the formula(m ∈ S.out −→ (m ∈ S.out U m ∈ R.in)).• If we assume that no message occurs twice in S.out then the asynchronous behaviorof a FIFO channel ensures that the property “message m cannot be in both buffersat the same time”.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
