| 摘要 | 第5-7页 |
| ABSTRACT | 第7-9页 |
| List of Abbreviations | 第12-17页 |
| Chapter 1 Introduction | 第17-29页 |
| 1.1 Formal Verification | 第17-19页 |
| 1.1.1 Model Checking | 第18页 |
| 1.1.2 Theorem Proving | 第18-19页 |
| 1.2 Temporal Logic and Temporal Logic Programming | 第19-23页 |
| 1.2.1 Temporal Logic | 第19-21页 |
| 1.2.2 Temporal Logic Programming | 第21-23页 |
| 1.3 Constraint Solving | 第23-24页 |
| 1.4 Motivation and Contributions | 第24-27页 |
| 1.5 The Organization of the Thesis | 第27-29页 |
| Chapter 2 MSVL and the Underlying Logic | 第29-41页 |
| 2.1 Projection Temporal Logic | 第29-35页 |
| 2.1.1 Syntax | 第29-30页 |
| 2.1.2 Semantics | 第30-31页 |
| 2.1.3 Derived Formulas | 第31-33页 |
| 2.1.4 Precedence Rules | 第33页 |
| 2.1.5 Replacement | 第33-34页 |
| 2.1.6 Logical Laws | 第34页 |
| 2.1.7 Propositional Projection Temporal Logic | 第34-35页 |
| 2.2 MSVL | 第35-40页 |
| 2.2.1 Expressions and Statements | 第35-38页 |
| 2.2.2 Normal Form | 第38-39页 |
| 2.2.3 Minimal Model Semantics of MSVL | 第39-40页 |
| 2.3 Conclusion | 第40-41页 |
| Chapter 3 Integration of Linear Constraints with MSVL | 第41-65页 |
| 3.1 Linear Constraints in MSVL | 第41-45页 |
| 3.1.1 Linear Constraint Statements | 第41-43页 |
| 3.1.2 Derived Statements | 第43页 |
| 3.1.3 Semi-Normal Form | 第43-45页 |
| 3.2 Two Issues | 第45-46页 |
| 3.2.1 Underlying Store | 第45页 |
| 3.2.2 How to Determine Current Values of Variables | 第45-46页 |
| 3.3 Operational Semantics | 第46-53页 |
| 3.3.1 Operational Semantics of MSVL | 第47-49页 |
| 3.3.2 Operational Semantics of Linear Constraints | 第49-53页 |
| 3.4 Soundness of the Operational Semantics | 第53-58页 |
| 3.5 Applications | 第58-61页 |
| 3.5.1 Truck Packing Problem | 第58-59页 |
| 3.5.2 Production Scheduling Problem | 第59-61页 |
| 3.6 Related Work | 第61-63页 |
| 3.7 Conclusion | 第63-65页 |
| Chapter 4 Solving a Specific Kind of CSPs with MSVL | 第65-85页 |
| 4.1 Features of a Specific Kind of CSPs | 第65-67页 |
| 4.2 Invoking of External Solvers | 第67-78页 |
| 4.2.1 Solving Constraints with SMT Solvers | 第68-72页 |
| 4.2.2 Solving Constraints with MIP Solvers | 第72-76页 |
| 4.2.3 Solving Constraints with CP Solvers | 第76-78页 |
| 4.3 Embedding Linear Constraints into MSV | 第78-81页 |
| 4.4 An Application:the Coins Problem | 第81-84页 |
| 4.4.1 Modeling and Solving with the Extended MSVL | 第81-82页 |
| 4.4.2 Comparison with ECL~iPS~e | 第82-84页 |
| 4.5 Conclusion | 第84-85页 |
| Chapter 5 Verification of Distributed Systems with MSVL | 第85-113页 |
| 5.1 Axiomatic Semantics of MSVL | 第85-89页 |
| 5.2 Asynchronous Communication Commands | 第89-90页 |
| 5.3 Asynchronous Communication Axioms | 第90-95页 |
| 5.3.1 State Axioms for Asynchronous Communication | 第90-94页 |
| 5.3.2 Derived Theorems | 第94-95页 |
| 5.4 Soundness and Completeness | 第95-100页 |
| 5.5 An Application:Ricart-Agrawala Algorithm | 第100-110页 |
| 5.5.1 Description | 第100-101页 |
| 5.5.2 Modeling | 第101-102页 |
| 5.5.3 Properties | 第102-106页 |
| 5.5.4 Verification | 第106-110页 |
| 5.6 Related Work | 第110-111页 |
| 5.7 Conclusion | 第111-113页 |
| Chapter 6 Some Fixed-point Issues in PPTL | 第113-137页 |
| 6.1 Two Kinds of Index Set Expressions | 第113-118页 |
| 6.2 Fixed-points of Equation X≡Q ∨P∧○X | 第118-126页 |
| 6.3 Some Well-formed Instances | 第126-131页 |
| 6.4 Fixed-point Issues in Propositional Linear Temporal Logic | 第131-135页 |
| 6.4.1 Syntax and Semantics of PLTL | 第131-132页 |
| 6.4.2 Fixed-point Issues of PLTL | 第132-133页 |
| 6.4.3 A Transformation from PLTL to PPTL | 第133-135页 |
| 6.5 Conclusion | 第135-137页 |
| Chapter 7 Conclusions and Future Works | 第137-141页 |
| 7.1 Conclusions | 第137-140页 |
| 7.2 Future Works | 第140-141页 |
| REFERENCES | 第141-149页 |
| ACKNOWLEDGEMENTS | 第149-151页 |
| BIOGRAPHY | 第151-153页 |
| 1. Personal Profile | 第151页 |
| 2. Educational Background | 第151页 |
| 3. Research Achievement | 第151-153页 |
| APPENDIX | 第153-161页 |
