5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 49
Текст из файла (страница 49)
Temporal logic is aformalism par excellence for treating these aspects. Temporal logic extends propositionalor predicate logic by modalities that permit to referral to the infinite behavior of a reactivesystem. They provide a very intuitive but mathematically precise notation for expressingproperties about the relation between the state labels in executions, i.e., LT properties.Temporal logics and related modal logics have been studied in ancient times in differentareas such as philosophy.
Their application to verifying complex computer systems wasproposed by Pnueli in the late seventies.In this monograph, we will focus our attention on propositional temporal logics, i.e., extensions of propositional logic by temporal modalities. These logics should be distinguishedfrom first- (or higher-) order temporal logics that impose temporal modalities on top of229230Linear Temporal Logicpredicate logic. Throughout this monograph we assume some familiarity with the basicprinciples of propositional logic. A brief introduction and summary of our notations canbe found in Appendix A.3.
The elementary temporal modalities that are present in mosttemporal logics include the operators:♦“eventually” (eventually in the future)“always” (now and forever in the future)The underlying nature of time in temporal logics can be either linear or branching. Inthe linear view, at each moment in time there is a single successor moment, whereasin the branching view it has a branching, tree-like structure, where time may split intoalternative courses.
This chapter considers LTL (Linear Temporal Logic), a temporal logicthat is based on a linear-time perspective. Chapter 6 introduces CTL (Computation TreeLogic), a logic that that is based on a branching-time view. Several model-checking toolsuse LTL (or a slight variant thereof) as a property specification language. The modelchecker SPIN is a prominent example of such an automated verification tool. One of themain advantages of LTL is that imposing fairness assumptions (such as strong and weakfairness) does not require the use of any new machinery: the typical fairness assumptionscan all be specified in LTL.
Verifying LTL-formulae under fairness constraints can be doneusing the algorithm for LTL. This does not apply to CTL.Before introducing LTL in more detail, a short comment on the adjective “temporal” is inorder to avoid any possible confusion. Although the term temporal suggests a relationshipwith the real-time behavior of a reactive system, this is only true in an abstract sense. Atemporal logic allows for the specification of the relative order of events. Some examplesare “the car stops once the driver pushes the brake”, or “the message is received afterit has been sent”.
It does however not support any means to refer to the precise timingof events. The fact that there is a minimal delay of at least 3 μs between braking andthe actual halting of the car cannot be specified. In terms of transition systems, neitherthe duration of taking a transition nor state residence times can be specified using theelementary modalities of temporal logics. Instead, these modalities do allow for specifyingthe order in which state labels occur during an execution, or to assess that certain statelabels occur infinitely often in a (or all) system execution.
One might thus say that themodalities in temporal logic are time-abstract.As will be discussed in this chapter, LTL may be used to express the timing for the classof synchronous systems in which all components proceed in a lock-step fashion. In thissetting, a transition corresponds to the advance of a single time-unit. The underlyingtime domain is thus discrete, i.e., the present moment refers to the current state andthe next moment corresponds to the immediate successor state. Stated differently, thesystem behavior is assumed to be observable at the time points 0, 1, 2, .
. .. The treatmentLinear Temporal Logic231of real-time constraints in asynchronous systems by means of a continuous-time domainwill be discussed in Chapter 9 where a timed version of CTL, called Timed CTL, will beintroduced. Table 5.1 summarizes the distinguishing features of the main temporal logicsconsidered in this monograph.logicLTLCTLTimed CTLlinear-time(path-based)√branching-time(state-based)real-time requirements(continuous-time domain)√√√Table 5.1: Classification of the temporal logics in this monograph.5.1.1SyntaxThis subsection describes the syntactic rules according to which formulae in LTL canbe constructed. The basic ingredients of LTL-formulae are atomic propositions (statelabels a ∈ AP), the Boolean connectors like conjunction ∧, and negation ¬, and twobasic temporal modalities (pronounced “next”) and U (pronounced “until”). Theatomic proposition a ∈ AP stands for the state label a in a transition system.
Typically,the atoms are assertions about the values of control variables (e.g., locations in programgraphs) or the values of program variables such as ”x > 5” or ”x y”. The -modalityis a unary prefix operator and requires a single LTL formula as argument. Formula ϕholds at the current moment, if ϕ holds in the next “step”. The U -modality is a binaryinfix operator and requires two LTL formulae as argument. Formula ϕ1 U ϕ2 holds at thecurrent moment, if there is some future moment for which ϕ2 holds and ϕ1 holds at allmoments until that future moment.Definition 5.1.Syntax of LTLLTL formulae over the set AP of atomic proposition are formed according to the followinggrammar:1ϕ ::= trueaϕ1 ∧ ϕ2 ¬ϕϕϕ1 U ϕ2where a ∈ AP.1The Backus Naur form (BNF) is used in a somewhat liberal way.
More concretely, nonterminals areidentified with derived words (formulae) and indices in the rules. Moreover, brackets will be used, e.g. ina ∧ (b U c), which are not shown in the grammar. Such simplified notations for grammars to determine thesyntax of formulae of some logic (or terms of other calculi) are often called abstract syntax.232Linear Temporal LogicWe mostly abstain from explicitly indicating the set AP of propositions as this followseither from the context or can be defined as the set of atomic propositions occurring inthe LTL formula at hand.The precedence order on the operators is as follows. The unary operators bind strongerthan the binary ones. ¬ and bind equally strong. The temporal operator U takesprecedence over ∧, ∨, and →.
Parentheses are omitted whenever appropriate, e.g., we write¬ϕ1 U ϕ2 instead of (¬ϕ1 ) U ( ϕ2 ). Operator U is right-associative, e.g., ϕ1 U ϕ2 U ϕ3stands for ϕ1 U (ϕ2 U ϕ3 ).Using the Boolean connectives ∧ and ¬, the full power of propositional logic is obtained.Other Boolean connectives such as disjunction ∨, implication →, equivalence ↔, and theparity (or: exclusive or) operator ⊕ can be derived as follows:ϕ1 ∨ ϕ2ϕ1 → ϕ2ϕ1 ↔ ϕ2ϕ1 ⊕ ϕ2def==def=def=...def¬(¬ϕ1 ∧ ¬ϕ2 )¬ϕ1 ∨ ϕ2(ϕ1 → ϕ2 ) ∧ (ϕ2 → ϕ1 )(ϕ1 ∧ ¬ϕ2 ) ∨ (ϕ2 ∧ ¬ϕ1 )The until operator allows to derive the temporal modalities ♦ (“eventually”, sometimesin the future) and (“always”, from now on forever) as follows:♦ϕ = true U ϕdefϕ = ¬♦¬ϕdefAs a result, the following intuitive meaning of ♦ and is obtained.
♦ϕ ensures that ϕwill be true eventually in the future. ϕ is satisfied if and only if it is not the case thateventually ¬ϕ holds. This is equivalent to the fact that ϕ holds from now on forever.Figure 5.1 sketches the intuitive meaning of temporal modalities for the simple case inwhich the arguments of the modalities are just atomic propositions from { a, b }. On theleft-hand side, some LTL formulae are indicated, whereas on the right hand side sequencesof states (i.e., paths) are depicted.By combining the temporal modalities ♦ and , new temporal modalities are obtained.For instance, ♦a (“always eventually a”) describes the (path) property stating that atany moment j there is a moment i j at which an a-state is visited. This thus amountsto assert that an a-state is visited infinitely often. The dual modality ♦a expresses thatfrom some moment j on, only a-states are visited.
So:♦ϕ“infinitely often ϕ”♦ϕ“eventually forever ϕ”Linear Temporal Logic233aarbitraryarbitraryarbitraryarbitrary...atomic prop. aarbitraryaarbitraryarbitraryarbitrarynext step a...a ∧ ¬ba ∧ ¬ba ∧ ¬bbarbitrary...until a U beventually ♦a¬a¬a¬aaarbitrary...aaaaaalways a...Figure 5.1: Intuitive semantics of temporal modalities.Before proceeding with the formal semantics of LTL, we present some examples.Example 5.2.Properties for the Mutual Exclusion ProblemConsider the mutual exclusion problem for two concurrent processes P1 and P2 , say.
Process Pi is modeled by three locations: (1) the noncritical section, (2) the waiting phasewhich is entered when the process intends to enter the critical section, and (3) the criticalsection. Let the propositions waiti and criti denote that process Pi is in its waiting phaseand critical section, respectively.The safety property stating that P1 and P2 never simultaneously have access to theircritical sections can be described by the LTL-formula:( ¬ crit1 ∨ ¬ crit2 ).This formula expresses that always () at least one of the two processes is not in its criticalsection (¬criti ).The liveness requirement stating that each process Pi is infinitely often in its critical234Linear Temporal Logicsection is described by the LTL formula:(♦crit1 ) ∧ (♦crit2 ).The weakened form that every waiting process will eventually enter its critical section(i.e., starvation freedom) can—by using the additional proposition waiti —be formulatedas follows:(♦wait1 → ♦crit1 ) ∧ (♦wait2 → ♦crit2 ).These formulae only refer to the locations (i.e., values of the program counters) by theatomic propositions waiti and criti .
Propositions can however also refer to program variables. For instance, for the solution of the mutual exclusion problem using a binarysemaphore y, the formula:((y = 0) → crit1 ∨ crit2 )states that whenever the semaphore y has the value 0, one of the processes is in its criticalsection.Example 5.3.Properties for the dining philosophersFor the dining philosophers (see Example 3.2 on page 90) deadlock freedom can be described by the LTL formulawaiti ∧occupiedi ).¬(0i<n0i<nWe assume here that there are n philosophers and chop sticks, indexed from 0 to n−1.The atom waiti means that philosopher i waits for one of the sticks on his left or right,but keeps the other one in his hand. Similarly, occupiedi indicates that stick i is in use.Example 5.4.Properties for a Traffic LightFor a traffic light with the phases ”green”, ”red” and ”yellow”, the liveness property♦green expresses that the traffic light is infinitely often green.
A specification of thetraffic light cycles and their chronological order can be provided by means of a conjunctionof LTL-formulae stating the predecessor phase of any phase. For instance, the requirement“once red, the light cannot become green immediately” can be expressed by the LTLformula(red → ¬ green).The requirement “once red, the light always becomes green eventually after being yellowfor some time” is expressed by(red → (red U (yellow ∧ (yellow U green)))).Linear Temporal Logic235A progress property like “every request will eventually lead to a response” can be describedby the following formula of the type(request → ♦response).Remark 5.5.Length of a FormulaLet | ϕ | denote the length of LTL formula ϕ in terms of the number of operators in ϕ.This can easily be defined by induction on the structure of ϕ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
