5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 23
Текст из файла (страница 23)
A path fragment is called initial if it starts in an initial state,i.e., if s0 ∈ I.A maximal path fragment is a path fragment that cannot be prolonged: either it is infiniteor it is finite but ends in a state from which no transition can be taken. Let Paths(s) denotethe set of maximal path fragments π with first(π) = s, and Pathsfin (s) denote the set ofall finite path fragments π with first(π ) = s.Definition 3.6.PathA path of transition system TS is an initial, maximal path fragment.2Let Paths(TS) denote the set of all paths in TS, and Pathsfin (TS) the set of all initial,finite path fragments of TS.Example 3.7.Beverage Vending MachineConsider the beverage vending machine of Example 2.2 on page 21.
For convenience, itstransition system is repeated in Figure 3.5. As the state labeling is simply L(s) = { s }for each state s, the names of states may be used in paths (as in this example), as well asatomic propositions (as used later on). Example path fragments of this transition systemareπ1 = pay select soda pay select soda .
. .π2 = select soda pay select beer . . .π = pay select soda pay select soda .These path fragments result from the execution fragments indicated in Example 2.8 onpage 25. Only π1 is a path. The infinite path fragment π2 is maximal but not initial.π is initial but not maximal since it is finite while ending in a state that has outgoing2It is important to realize the difference between the notion of a path in a transition system and thenotion of a path in a digraph. A path in a transition system is maximal, whereas a path in a digraph inthe graph-theoretical sense is not always maximal.
Besides, paths in a digraph are usually required to befinite whereas paths in transition systems may be infinite.Linear-Time Behavior97payget sodaget beerinsert coinsodaτselectτbeerFigure 3.5: A transition system of a simple beverage vending machine.transitions. We have that last(π ) = soda, first(π2 ) = select, π1 [0] = pay, π1 [3] = pay ,, π[..2] = π[3..], len(π ) = 5, and len(π1 ) = ∞.π1 [..5] = π3.2.2TracesExecutions (as introduced in Chapter 2) are alternating sequences consisting of statesand actions. Actions are mainly used to model the (possibility of) interaction, be itsynchronous or asynchronous communication. In the sequel, interaction is not our primeinterest, but instead we focus on the states that are visited during executions.
In fact, thestates themselves are not “observable”, but just their atomic propositions. Thus, ratherα0α1→ s1 −−→ s2 . . . we consider sequences of thethan having an execution of the form s0 −−form L(s0 ) L(s1 ) L(s2 ) . . . that register the (set of) atomic propositions that are valid alongthe execution. Such sequences are called traces.The traces of a transition system are thus words over the alphabet 2AP . In the followingit is assumed that a transition system has no terminal states. In this case, all traces areinfinite words. (Recall that the traces of a transition system have been defined as tracesinduced by its initial maximal path fragments.
See also Appendix A.2, page 912). Thisassumption is made for simplicity and does not impose any serious restriction. First of all,prior to checking any (linear-time) property, a reachability analysis could be carried out todetermine the set of terminal states. If indeed some terminal state is encountered, the system contains a deadlock and has to be repaired before any further analysis. Alternatively,each transition system TS (that probably has a terminal state) can be extended such that→ sstop , and sstop isfor each terminal state s in TS there is a new state sstop , transition s −→ sstop .
The resulting “equivalent” transition systemequipped with a self-loop, i.e., sstop −obviously has no terminal states.33A further alternative is to adapt the linear-time framework for transition systems with terminal states.The main concepts of this chapter are still applicable, but require some adaptions to distinguish nonmax-98Linear-Time PropertiesDefinition 3.8.Trace and Trace FragmentLet TS = (S, Act, →, I, AP, L) be a transition system without terminal states. The traceof the infinite path fragment π = s0 s1 . .
. is defined as trace(π) = L(s0 ) L(s1 ) . . .. The traceπ ) = L(s0 ) L(s1 ) . . . L(sn ).of the finite path fragment π = s0 s1 . . . sn is defined as trace(The trace of a path fragment is thus the induced finite or infinite word over the alphabet2AP , i.e., the sequence of sets of atomic propositions that are valid in the states of thepath.
The set of traces of a set Π of paths is defined in the usual way:trace(Π) = { trace(π) | π ∈ Π }.A trace of state s is the trace of an infinite path fragment π with first(π) = s. Accordingly,a finite trace of s is the trace of a finite path fragment that starts in s. Let Traces(s) denotethe set of traces of s, and Traces(TS) the set of traces of the initial states of transitionsystem TS:Traces(s) = trace(Paths(s))andTraces(TS) =Traces(s).s∈IIn a similar way, the finite traces of a state and of a transition system are defined:Tracesfin (s) = trace(Pathsfin (s))andTracesfin (TS) =Tracesfin (s).s∈IExample 3.9.Semaphore-Based Mutual ExclusionConsider the transition system TSSem as depicted in Figure 3.6.
This two-process mutualexclusion example has been described before in Example 2.24 (page 43).Assume the available atomic propositions are crit1 and crit2 , i.e.,AP = { crit1 , crit2 }.The proposition crit1 holds in any state of the transition system TSSem where the firstprocess (called P1 ) is in its critical section. Proposition crit2 has the same meaning forthe second process (i.e., P2 ).Consider the execution in which the processes P1 and P2 enter their critical sections inan alternating fashion.
Besides, they only request to enter the critical section when theimal and maximal finite paths.Linear-Time Behavior99n1 , n2 , y=1w1 , n2 , y=1c1 , n2 , y=0n1 , w2 , y=1w1 , w2 , y=1c1 , w2 , y=0n1 , c2 , y=0w1 , c2 , y=0Figure 3.6: Transition system of semaphore-based mutual exclusion algorithm.other process is no longer in its critical section. Situations in which one process is in itscritical section whereas the other is moving from the noncritical state to the waiting stateare impossible.The path π in the state graph of TSSem where process P1 is the first to enter its criticalsection is of the formπ=n1 , n2 , y = 1 → w1 , n2 , y = 1 → c1 , n2 , y = 0 →n1 , n2 , y = 1 → n1 , w2 , y = 1 → n1 , c2 , y = 0 → .
. .The trace of this path is the infinite word:trace(π) = ∅ ∅ { crit1 } ∅ ∅ { crit2 } ∅ ∅ { crit1 } ∅ ∅ { crit2 } . . . .The trace of the finite path fragmentπ=n1 , n2 , y = 1 → w1 , n2 , y = 1 → w1 , w2 , y = 1 →w1 , c2 , y = 0 → w1 , n2 , y = 1 → c1 , n2 , y = 0is trace(π ) = ∅ ∅ ∅ { crit2 } ∅ { crit1 }.1003.2.3Linear-Time PropertiesLinear-Time PropertiesLinear-time properties specify the traces that a transition system should exhibit. Informally speaking, one could say that a linear-time property specifies the admissible (ordesired) behavior of the system under consideration.
In the following we provide a formaldefinition of such properties. This definition is rather elementary, and gives a good basicunderstanding of what a linear-time property is. In Chapter 5, a logical formalism will beintroduced that allows for the specification of linear-time properties.In the following, we assume a fixed set of propositions AP. A linear-time (LT) property isa requirement on the traces of a transition system. Such property can be understood as arequirement over all words over AP, and is defined as the set of words (over AP) that areadmissible:Definition 3.10.LT PropertyA linear-time property (LT property) over the set of atomic propositions AP is a subsetof (2AP )ω .Here, (2AP )ω denotes the set of words that arise from the infinite concatenation of wordsin 2AP .
An LT property is thus a language (set) of infinite words over the alphabet 2AP .Note that it suffices to consider infinite words only (and not finite words), as transitionsystems without terminal states are considered. The fulfillment of an LT property by atransition system is defined as follows.Definition 3.11.Satisfaction Relation for LT PropertiesLet P be an LT property over AP and TS = (S, Act, →, I, AP, L) a transition systemwithout terminal states. Then, TS = (S, Act, →, I, AP, L) satisfies P , denoted TS |= P ,iff Traces(TS) ⊆ P . State s ∈ S satisfies P , notation s |= P , whenever Traces(s) ⊆ P .Thus, a transition system satisfies the LT property P if all its traces respect P , i.e., if allits behaviors are admissible. A state satisfies P whenever all traces starting in this statefulfill P .Example 3.12.Traffic LightsConsider two simplified traffic lights that only have two possible settings: red and green.Let the propositions of interest beAP = { red1 , green1 , red2 , green2 }Linear-Time Behavior101green2red1ααgreen1αred1 , green2 αααgreen1 , red2 red2Figure 3.7: Two fully synchronized traffic lights (left and middle) and their parallel composition (right).We consider two LT properties of these traffic lights and give some example words thatare contained by such properties.
First, consider the property P that states:“The first traffic light is infinitely often green”.This LT property corresponds to the set of infinite words of the form A0 A1 A2 . . . over2AP , such that green1 ∈ Ai holds for infinitely many i.
For example, P contains theinfinite words{ red1 , green2 } { green1 , red2 } { red1 , green2 } { green1 , red2 } . . . ,∅ { green1 } ∅ { green1 } ∅ { green1 } ∅ { green1 } ∅ . . .{ red1 , green1 } { red1 , green1 } { red1 , green1 } { red1 , green1 } . . .and{ green1 , green2 } { green1 , green2 } { green1 , green2 } { green1 , green2 } . . .The infinite word { red1 , green1 } { red1 , green1 } ∅ ∅ ∅ ∅ .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
