5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 61
Текст из файла (страница 61)
. Bn+m−1 , and the subformulae ψ2 that appear on the right hand side of an untilsubformula of ϕ and are contained in some of the sets Bn , . . . Bn+m−1 . This additional296Linear Temporal Logicinformation requires O(|ϕ|) space. Thus, the above nondeterministic algorithm can berealized in a polynomially space-bounded way.By Lemma 5.47 and Theorem 5.46 we get:Theorem 5.48.The LTL model-checking problem is PSPACE-complete.5.2.2LTL Satisfiability and Validity CheckingThe last section of this chapter considers the satisfiability problem and the validity problemfor LTL. The satisfiability problem is: for a given LTL formula ϕ, does there exist a modelfor which ϕ holds? That is, do we have Words(ϕ) = ∅? Satisfiability can be solved byconstructing an NBA Aϕ for LTL formula ϕ.
In this way, the existence of an infinite wordσ ∈ Words(ϕ) = Lω (Aϕ ) can be established. The emptiness problem for NBA A , i.e.,whether Lω (A) = ∅ or not, can be solved by means of a technique similar to persistencechecking, see Algorithm 12.
In addition to an affirmative response, a prefix of a wordσ ∈ Lω (A) = Words(ϕ) can be provided similar to a counterexample for model checkingLTL.Algorithm 12 Satisfiability checking for LTLInput: LTL formula ϕ over APOutput: “yes” if ϕ is satisfiable. Otherwise “no”.Construct an NBA A = (Q, 2AP , δ, Q0 , F ) with Lω (A) = Words(ϕ)(* Check whether Lω (A) = ∅.
*)Perform a nested DFS to determine whether there exists a state q ∈ F reachable fromq0 ∈ Q0 and that lies on a cycleIf so, then return “yes”. Otherwise, “no”.Given that satisfiability for LTL can be tackled using similar techniques as for modelchecking LTL, let us now consider the validity problem. Formula ϕ is valid whenever ϕholds under all interpretations, i.e., ϕ ≡ true.
For LTL formula ϕ over AP we have ϕ isvalid if and only if Words(ϕ) = (2AP )ω . The validity of ϕ can be established by using theAutomata-Based LTL Model Checking297observation that ϕ is valid if and only if ¬ϕ is not satisfiable. Hence, to algorithmicallycheck whether ϕ is obtained, one constructs an NBA for ¬ϕ and applies the satisfiablityalgorithm (see Algorithm 12) to ¬ϕ.The outlined LTL satisfiability algorithm has a runtime that is exponential in the lengthof ϕ. The following result shows that an essentially more efficient technique cannot beachieved as both the validity and satisfiability problems are PSPACE-hard. In fact, bothproblems are even PSPACE-complete. Membership to PSPACE for the LTL satisfiabilityproblem can be shown by providing a nondeterministic polynomially space-bounded algorithm that guesses a finite run in the GNBA Gϕ for the given formula ϕ and checks whetherthis finite run is a prefix of an accepting run in Gϕ .
The details are skipped here sincethey are very similar to the algorithm we provided for the existential LTL model checkingproblem (see Lemma 5.47 on page 294). The fact that the LTL validity problem belongsto PSPACE can be derived from the observations that ϕ is valid iff ¬ϕ is not satisfiableand that PSPACE is closed under complementation. We now focus on the proof for thePSPACE-hardness.Theorem 5.49.LTL Satisfiability and Validity (Lower Bound)The satisfiability and validity problems for LTL are PSPACE-hard.Proof: Since satisfiability and validity are complementary in the sense that ϕ is satisfiableif and only if ¬ϕ is not valid, and vice versa, it suffices to show the PSPACE-hardnessof the satisfiability problem.
This is done by providing a polynomial reduction from theexistential variant of the LTL model-checking problem (see the proof of Theorem 5.46 onpage 290) to the satisfiability problem for LTL.Let TS = (S, Act, →, I, AP, L) be a finite transition system and ϕ an LTL formula overAP. The goal is to construct an LTL formula ψ such that ψ is satisfiable if and only ifthere is a path π in TS with π |= ϕ. Besides, ψ should be constructed in polynomial time.The atomic propositions in ψ are elements in AP = AP S. For any state s ∈ S leta ∧¬a.Φs =a∈L(s)a∈L(s)/The formula Φs can be viewed as a characteristic formula for the labeling of s, sinces |= Φs if and only if L(s) = L(s ), for any s ∈ S.
However, for the LTL satisfiabilityproblem, there is no fixed transition system and Φs can hold" also for other states (inanother transition system). For s ∈ S and T ⊆ S, let ΨT = t∈T t be the characteristicformula for the set T . Letψs = s → (Φs ∧ ΨP ost(s) )298Linear Temporal Logicassert that in state s, the labels L(s) hold, and that transitions exist to any of its immediatesuccessors Post(s). Let!(s ∧¬t).Ξ =s∈St∈S\{ s }Stated in words, Ξ asserts that exactly one of the atomic propositions s ∈ AP holds.These definitions constitute the ingredients for the definition of ψ.
For set I of initialstates, letψs ∧ ϕ.ψ = ΨI ∧ Ξ ∧ ΨS ∧s∈SIt follows directly that ψ can be derived from TS and ϕ in polynomial time. It remainsto show that∃π ∈ Paths(TS). π |= ϕif and only if ψ is satisfiable.⇒: Let π = s0 s1 s2 . . . be an initial, infinite path in TS with π |= ϕ. Now consider π asa path in the transition system TS that agrees with TS but uses the extended labelingfunction L (s) = L(s) ∪ { s }.
Then, π |= ΨI , since s0 ∈ I. In addition, π |= Ξ andπ |= ψs since Ξ and ψs hold in all states of TS . Thus, π |= ψ. Hence, π is a witness forthe satisfiability of ψ.⇐: Assume ψ is satisfiable. Let A0 A1 A2 . . . be an infinite word over the alphabet 2APwith A0 A1 A2 . . . ∈ Words(ψ). SinceA0 A1 A2 . . . |= Ξthere is a unique state sequence π = s0 s1 s2 . .
. in TS with si ∈ Ai for all i 0. SinceA0 A1 A2 . . . |= ΨI , we get s0 ∈ I. Asψs ,A0 A1 A2 . . . |= s∈Swe have Ai ∩ AP = L(si ) and si+1 ∈ Post(si ) for all i 0. This yields that π is a path inTS and π |= ϕ.5.3Summary• Linear Temporal Logic (LTL) is a logic for formalizing path-based properties.• LTL formulae can be transformed algorithmically into nondeterministic Büchi automata (NBA). This transformation can cause an exponential blowup.Bibliographic Notes299• The presented algorithm for the construction of an NBA for a given LTL formulaϕ relies on first constructing a GNBA for ϕ, which is then transformed into anequivalent NBA.• The GNBA for ϕ encodes the semantics of propositional logic and the semantics ofthe next-step operator in its transitions.
Based on the expansion law, the meaningof until is split into local requirements (encoded by the states of a GNBA), next-steprequirements (encoded by the transitions of the GNBA), and a fairness condition(encoded by the acceptance sets of the GNBA).• LTL formulae describe ω-regular LT properties, but do not have the same expressiveness as ω-regular languages.• The LTL model-checking problem can be solved by a nested depth-first search in theproduct of the given transition system and an NBA for the negated formula.• The time complexity of the automata-based model-checking algorithm for LTL islinear in the size of the transition system and exponential in the length of the formula.• Fairness assumptions can be described by LTL formulae.
The model-checking problem for LTL with fairness assumptions is reducible to the standard LTL modelchecking problem.• The LTL model-checking problem is PSPACE-complete.• Satisfiability and validity of LTL formulae can be solved via checking emptinessof nondeterministic Büchi automata.
The emptiness check can be determined by anested DFS that checks the existence of a reachable cycle containing an accept state.Both problems are PSPACE-complete.5.4Bibliographic NotesLinear temporal logic. Based on prior work on modal logics and temporal modalities[270, 345, 244, 230], Pnueli introduced (linear) temporal logics for reasoning about reactive systems in the late seventies in his seminal paper [337].
Since then, a variety ofvariants and extensions of LTL have been investigated, such as Lamport’s Temporal Logicof Actions (TLA) [260] and LTL with past operators [159, 274, 262]. LTL forms the basisfor the recently standardized industrial property specification language PSL [136]. Thepast extension of LTL does not change the expressiveness of LTL, but can be helpful forspecification convenience and modular reasoning. For several properties, the use of pastoperators may lead to (exponentially) more succinct formulae than in ordinary LTL.
To300Linear Temporal Logiccover the full class of ω-regular LT properties, Vardi and Wolper introduced an extensionof LTL by automata formulae [424, 425, 411, 412].LTL model checking. Vardi and Wolper also developed the automata-based model checkingalgorithm for LTL presented in this chapter.
The presented algorithm to construct an NBAfrom a given LTL formula is, in our opinion, the simplest and most intuitive one. In themeantime, various alternative techniques have been developed that generate more compactNBAs or that attempt to minimize a given NBA, see e.g. [166, 110, 148, 375, 162, 149,167, 157, 389, 369]. Alternative LTL model-checking algorithms that do not use Büchiautomata, but a so-called tableau for the LTL formula, were presented by Lichtenstein andPnueli [273] and Clarke, Grumberg, and Hamaguchi [88]. The results about the complexityof LTL model checking and the satisfiability problem are due to Sistla and Clarke [372].There is a variety of surveys and textbooks; see, e.g.,[245, 138, 173, 283, 158, 284, 92, 219,379, 365], where several other aspects of LTL and related logics, such as deductive proofsystems, alternative model-checking algorithms, or more details about the expressiveness,are treated.Examples.
The garbage collection algorithm presented in Example 5.31 is due to Ben-Ari[41]. Several leader election protocols that fit into the shape of Example 5.13 have beensuggested; see, e.g., [280].LTL model checkers. SPIN is the most well-known LTL model checker and has beendeveloped by Holzmann [209]. Transition systems are described in the modeling languagePromela, and LTL formulae are checked using the algorithm advocated by Gerth et al.[166]. LTL model checking using a tableau construction is supported by NuSMV [83].5.5ExercisesExercise 5.1.
Consider the following transition system over the set of atomic propositions { a, b }:s4{b}{a}{a}s1s2s3{ a, b }Indicate for each of the following LTL formulae the set of states for which these formulae areExercises301fulfilled:(a) a(d) ♦ a(b) a(e) (b U a)(c) b(f) ♦ (a U b)Exercise 5.2.{ a, b, c }:Consider the transition system TS over the set of atomic propositions AP ={a}s1s3{b, c}{c}s4{b}s2s5{a, b, c}Decide for each of the LTL formulae ϕi below, whether T S |= ϕi holds. Justify your answers! IfT S |= ϕi , provide a path π ∈ P aths(T S) such that π |= ϕi .ϕ1ϕ2ϕ3ϕ4ϕ5ϕ6= ♦c= ♦c= ¬c → c= a= a U (b ∨ c)= ( b) U (b ∨ c)Exercise 5.3. Consider the sequential circuit in Figure 5.24 and let AP = { x, y, r1 , r2 }.
ProvideLTL formulae for the following properties:xyr_1,r_2Figure 5.24: Circuit for Exercise 5.3.302Linear Temporal Logic(a) “It is impossible that the circuit outputs two successive 1s.”(b) “Whenever the input bit is 1, in at most two steps the output bit will be 1.”(c) “Whenever the input bit is 1, the register bits do not change in the next step.”(d) “Register r1 has infinitely often the value 1.”Determine which of these properties are satisfied for the initial register evaluation where r1 = 0and r2 = 0? Justify your answers.Exercise 5.4. Suppose we have two users, Peter and Betsy, and a single printer device Printer.Both users perform several tasks, and every now and then they want to print their results on thePrinter. Since there is only a single printer, only one user can print a job at a time.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
