Lecture 5: Model Checking General LTL A. PnueliModel Checking General Temporal FormulasNext, we consider methods for model checking general LTL formulas.Let D be an FDS andϕan LTL formula. Assume we wish to check whether D |=ϕ.We proceed along the following steps:• Construct a temporal acceptor A(¬ϕ). This is an FDS whose computations areall the sequences falsifyingϕ.• Form the parallel composition D k| A(¬ϕ). This is an FDS whose computationsare all computations of D which violateϕ.• Check whether the composition D k| A(¬ϕ) is feasible. D |=ϕiff D k| T (¬ϕ) isinfeasible.It only remains to describe the construction of an acceptor A(ψ) for a general LTLformula ψ.Analysis of Reactive Systems, NYU, Spring, 2006 75Lecture 5: Model Checking General LTL A. PnueliOperations on FDS’s: Asynchronous Parallel CompositionThe asynchronous parallel composition of systems D1and D2, denoted byD1k D2, is given by D = hV, Θ, ρ, J , Ci, whereV = V1∪ V2Θ = Θ1∧ Θ2ρ =(ρ1∧ pres(V2− V1))∨ (ρ2∧ pres(V1− V2))J = J1∪ J2C = C1∪ C2The predicate pres(U) stands for the assertion U′= U , implying that all thevariables in U are preserved by the transition.Asynchronous parallel composition represents the interleaving-based concurrencywhich is the assumed concurrency in shared-variables models.Claim 7. D(P1k P2) ∼ D(P1) k D(P2)That is, the FDS corresponding to the program P1k P2is equivalent to theasynchronous parallel composition of the FDS’s corresponding to P1and P2.Analysis of Reactive Systems, NYU, Spring, 2006 76Lecture 5: Model Checking General LTL A. PnueliSynchronous Parallel CompositionThe synchronous parallel composition of systems D1and D2, denoted D1k| D2,is given by the FDS D = hV, Θ, ρ, J , Ci, whereV = V1∪ V2Θ = Θ1∧ Θ2ρ = ρ1∧ ρ2J = J1∪ J2C = C1∪ C2Synchronous parallel composition can be used for hardware verification, where itis the natural operator for combining two circuits into a composed circuit. Here weuse it for model checking of LTL formulas.Claim 8. The sequence σ of V -states is a computation of the combined D1k| D2iff σ ⇓V1is a computation of D1and σ ⇓V2is a computation of D2.Here, σ ⇓Videnotes the sequence obtained from σ by restricting each of the statesto a Vi-state.Analysis of Reactive Systems, NYU, Spring, 2006 77Lecture 5: Model Checking General LTL A. PnueliTemporal TestersThe building blocks from which we construct acceptors are temporal testers. Letϕbe a temporal formula over vocabulary U, and let x 6∈ U be a boolean variabledisjoint from U.In the following, let σ : s0, s1, . . . be an infinite sequence of states over U ∪ {x}.We say that x matchesϕin σ if, for every position j ≥ 0, the value of x at positionj is true iff (σ, j) |=ϕ.A temporal tester forϕis an FDS T (ϕ) over U ∪ {x}, satisfying the requirement:The infinite sequence σ is a computation of T (ϕ) iff x matchesϕin σ.A consequence of this definition is that every infinite sequence π of U-states canbe extended into a computation σ of T (ϕ) by interpreting x at position j ≥ 0 of σas 1 iff (π, j) |=ϕ.We can view T (ϕ) as a (possibly non-deterministic) transducer whichincrementally reads the values of the variables U and outputs in x the currentvalue ofϕover the infinite sequence.Analysis of Reactive Systems, NYU, Spring, 2006 78Lecture 5: Model Checking General LTL A. PnueliConstruction of Temporal TestersA formulaϕis called a principally temporal formula (PTF) if the main operator ofp is temporal. A PTF is called a basic temporal formula if it contains no other PTFas a proper sub-formula.We start our construction by presenting temporal testers for the basic temporalformulas.Analysis of Reactive Systems, NYU, Spring, 2006 79Lecture 5: Model Checking General LTL A. PnueliA Tester for pThe tester for the formula p is given by:T ( p) :V : Vars(p) ∪ {x}Θ : 1ρ : x = p′J = C : ∅Claim 9.T ( p) is a temporal tester for p.Proof:Let σ be a computation of T ( p). We will show that x matches p in σ. Letj ≥ 0 be any position. By the transition relation, x = 1 at position j iff sj+1|= p iff(σ, j) |= p.Let σ be an infinite sequence such that x matches p in σ. We will show thatσ is a computation of T ( p). For any position j ≥ 0, x = 1 at j iff (σ, j) |= p,iff sj+1|= p. Thus, x satisfies x = p′at every position j.Analysis of Reactive Systems, NYU, Spring, 2006 80Lecture 5: Model Checking General LTL A. PnueliA Tester for p U qThe tester for the formula p Uq is given by:T (p Uq) :V : Vars(p, q) ∪ {x}Θ : 1ρ : x = q ∨ (p ∧ x′)J : q ∨ ¬xC : ∅Claim 10. T (p Uq) is a temporal tester for p Uq.Proof:Let σ be a computation of T (p U q). We will show that x matches p U q in σ. Letj ≥ 0 be any position. Consider first the case that sj|= x and we will show that(σ, j) |= p Uq. According to the transition relation, sj|= x implies that either sj|= qor sj|= p and sj+1|= x. If sj|= q then (σ, j) |= p Uq and we are done. Otherwise,we apply the same argument to position j + 1. Continuing in this manner, weeither locate a k ≥ j such that sk|= q and si|= p for all i, j ≤ i < k, or we havesi|= ¬ q ∧ p ∧ x for all i ≥ j. If we locate a stopping k then, obviously (σ, j) |= p Uqaccording to the semantic definition of the U operator. The other case in whichboth ¬q and x hold over all positions beyond j is impossible since it violates thejustice requirement demanding that σ contains infinitely many positions at whicheither q is true or x is false.Analysis of Reactive Systems, NYU, Spring, 2006 81Lecture 5: Model Checking General LTL A. PnueliProof ContinuedNext we consider the case that σ is a computation of T (p U q) and (σ, j) |= p U q,and we have to show that sj|= x. According to the semantic definition, thereexists a k ≥ j such that sk|= q and si|= p for all i, j ≤ i < k. Proceeding fromk backwards all the way to j, we can show (by induction if necessary) that thetransition relation implies that st|= x for all t = k, k − 1, . . . , j.In the other direction, let σ be an infinite sequence such that x matches p Uq inσ. We will show that σ is a computation of T (p U q). From the semantic definitionof U it follows that (σ, j) |= p U q iff either sj|= q or sj|= p and (σ, j + 1) |= p U q.Thus, if x = (p Uq) at all positions, the transition relation x = q ∨ (p ∧ x′) holds atall positions. To show that x