# 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.**## Model Checking General Temporal Formulas

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

**View the full content.**View Full Document

## Model Checking General Temporal Formulas

0 0 66 views

Lecture Notes

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

**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