Lecture 5 Model Checking General LTL A Pnueli Model Checking General Temporal Formulas Next 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 are all the sequences falsifying Form the parallel composition D k A This is an FDS whose computations are all computations of D which violate Check whether the composition D k A is feasible D iff D k T is infeasible It only remains to describe the construction of an acceptor A for a general LTL formula Timed and Hybrid Systems NYU Spring 2007 79 Lecture 5 Model Checking General LTL A Pnueli Operations on FDS s Asynchronous Parallel Composition The asynchronous parallel composition of systems D1 and D2 denoted by D1 k D2 is given by D hV J Ci where V V1 V2 1 2 1 pres V2 V1 2 pres V1 V2 J J1 J2 C C1 C2 The predicate pres U stands for the assertion U U implying that all the variables in U are preserved by the transition Asynchronous parallel composition represents the interleaving based concurrency which is the assumed concurrency in shared variables models Claim 7 D P1 k P2 D P1 k D P2 That is the FDS corresponding to the program P1 k P2 is equivalent to the asynchronous parallel composition of the FDS s corresponding to P1 and P2 Timed and Hybrid Systems NYU Spring 2007 80 Lecture 5 Model Checking General LTL A Pnueli Synchronous Parallel Composition The synchronous parallel composition of systems D1 and D2 denoted D1 k D2 is given by the FDS D hV J Ci where V J C V1 1 1 J1 C1 V2 2 2 J2 C2 Synchronous parallel composition can be used for hardware verification where it is the natural operator for combining two circuits into a composed circuit Here we use it for model checking of LTL formulas Claim 8 The sequence of V states is a computation of the combined D1 k D2 iff V1 is a computation of D1 and V2 is a computation of D2 Here Vi denotes the sequence obtained from by restricting each of the states to a Vi state Timed and Hybrid Systems NYU Spring 2007 81 Lecture 5 Model Checking General LTL A Pnueli Temporal Testers The 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 variable disjoint 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 position j 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 can be 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 which incrementally reads the values of the variables U and outputs in x the current value of over the infinite sequence Timed and Hybrid Systems NYU Spring 2007 82 Lecture 5 Model Checking General LTL A Pnueli Construction of Temporal Testers A formula is called a principally temporal formula PTF if the main operator of p is temporal A PTF is called a basic temporal formula if it contains no other PTF as a proper sub formula We start our construction by presenting temporal testers for the basic temporal formulas Timed and Hybrid Systems NYU Spring 2007 83 Lecture 5 Model Checking General LTL A Pnueli A Tester for p The tester for the formula p is given by V Vars p x 1 T p 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 Let j 0 be any position By the transition relation x 1 at position j iff sj 1 p iff j p p in We will show that Let be an infinite sequence such that x matches 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 Timed and Hybrid Systems NYU Spring 2007 84 Lecture 5 Model Checking General LTL A Pnueli A Tester for p U q The tester for the formula p U q is given by V Vars p q x 1 x q p x T p U q J q x C Claim 10 T p U q is a temporal tester for p U q Proof Let be a computation of T p U q We will show that x matches p U q in Let j 0 be any position Consider first the case that sj x and we will show that j p U q According to the transition relation sj x implies that either sj q or sj p and sj 1 x If sj q then j p U q and we are done Otherwise we apply the same argument to position j 1 Continuing in this manner we either locate a k j such that sk q and si p for all i j i k or we have si q p x for all i j If we locate a stopping k then obviously j p U q according to the semantic definition of the U operator The other case in which both q and x hold over all positions beyond j is impossible since it violates the justice requirement demanding that contains infinitely many positions at which either q is true or x is false Timed and Hybrid Systems NYU Spring 2007 85 Lecture 5 Model Checking General LTL A Pnueli Proof Continued Next 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 there exists a k j such that sk q and si p for all i j i k Proceeding from k backwards all the way to j we can show by induction if necessary that the transition 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 U q in We will show that is a computation of T p U q From the semantic definition of 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 U q at all positions the transition relation x q p x holds at all positions To show that x satisfies the justice requirement q x it is enough to consider …
View Full Document
Unlocking...