| 摘要 | 第1-6页 |
| Abstract | 第6-13页 |
| 1 Introduction | 第13-25页 |
| ·Temporal Logic and Model Checking | 第13-18页 |
| ·Existing problems and Research Focuses | 第18-21页 |
| ·Thesis Overview and Contributions | 第21-25页 |
| 2 Background | 第25-35页 |
| ·Propositional Projection Temporal Logic | 第25-29页 |
| ·Model Checking Using Automata | 第29-31页 |
| ·ω-Automata | 第29-30页 |
| ·Specification using ω-Automata | 第30-31页 |
| ·Model Checking Using PPTL Specification | 第31-33页 |
| ·Summary | 第33-35页 |
| 3 Upper Bound of Complexity for PPTL | 第35-49页 |
| ·Inductive Method of Complete Normal Form | 第36-41页 |
| ·Definition of Complete Normal Graph | 第41-44页 |
| ·Upper bound of complexity for satisfiability of PPTL | 第44-48页 |
| ·Summary | 第48-49页 |
| 4 Stutter-invariant PPTL | 第49-71页 |
| ·Motivation of Introducing Stutter-invariance in PPTL | 第49-52页 |
| ·Stutter-Invariance of PPTL | 第52-57页 |
| ·Stutter-invariance | 第52-53页 |
| ·Stutter-invariant PPTL(PPTL_(st)) | 第53-56页 |
| ·Complexity of Determining Stutter-invariance | 第56-57页 |
| ·Case Study of Compositional Verification in PPTL_(st) | 第57-59页 |
| ·Partial-order Model-checking Using PPTL_(st) Specification | 第59-66页 |
| ·Compositional Verification of Automatic Gas Station | 第66-69页 |
| ·Summary | 第69-71页 |
| 5 Russian Cards Protocols | 第71-97页 |
| ·Russian Cards Problem | 第71-75页 |
| ·Russian Cards problem | 第71页 |
| ·What is a Safe Communication? | 第71-75页 |
| ·Generalization of Russian Cards Problem | 第75-92页 |
| ·Picking Rule | 第76-86页 |
| ·Construction of B~k in Row Case | 第76-82页 |
| ·Construction of B~k in Column Case | 第82-86页 |
| ·Deleting Rule | 第86-89页 |
| ·Safety Proof for R_((n)) in Row Case | 第89-91页 |
| ·Safety Proof for R_((n)) in Column Case | 第91-92页 |
| ·Example | 第92-95页 |
| ·R_((5)) in Row Case | 第92-95页 |
| ·Summary | 第95-97页 |
| 6 Verifying Russian Cards Protocol with PPTL_(st) | 第97-115页 |
| ·Modeling Russian Cards Protocol R_((3)) | 第97-104页 |
| ·The definition of the data structures and initial work | 第98-99页 |
| ·The definition of honest processes and an intruder | 第99-102页 |
| ·Safety property specified in PPTL_(st) | 第102-103页 |
| ·Correspondence of automaton and Never Claim | 第103-104页 |
| ·Partial-order model checking R_((3)) | 第104页 |
| ·Verification of R_((4)) and R_((5)) | 第104-114页 |
| ·Summary | 第114-115页 |
| 7 Conclusion and Future Work | 第115-119页 |
| Acknowledgements | 第119-121页 |
| References | 第121-131页 |
| Publications | 第131页 |
