NYU CSCI-GA 3033 - Model Checking General Temporal Formulas (20 pages)

Previewing pages 1, 2, 19, 20 of 20 page document View the full content.
View Full Document

Model Checking General Temporal Formulas



Previewing pages 1, 2, 19, 20 of actual document.

View the full content.
View Full Document
View Full Document

Model Checking General Temporal Formulas

66 views

Lecture Notes


Pages:
20
School:
New York University
Course:
Csci-Ga 3033 - Cloud Computing
Cloud Computing Documents

Unformatted text preview:

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 Analysis of Reactive Systems NYU Spring 2006 75 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 Analysis of Reactive Systems NYU Spring 2006 76 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



View Full Document

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Model Checking General Temporal Formulas and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Model Checking General Temporal Formulas and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?