| ABSTRACT | 第5-6页 |
| 摘要 | 第7-12页 |
| List of Symbols | 第12-14页 |
| List of Abbreviations | 第14-21页 |
| Chapter 1 Introduction | 第21-33页 |
| 1.1 Formal Verification | 第21-24页 |
| 1.1.1 Model Checking | 第22-23页 |
| 1.1.2 Automata | 第23-24页 |
| 1.2 Temporal Logic | 第24-27页 |
| 1.2.1 Linear Time μ-Calculus | 第25-26页 |
| 1.2.2 Temporal Logic in AI Planning | 第26-27页 |
| 1.3 Parity Games | 第27-29页 |
| 1.4 Contributions | 第29-31页 |
| 1.5 The Organization of the Thesis | 第31-33页 |
| Chapter 2 Preliminaries | 第33-43页 |
| 2.1 Syntax of νTL | 第33-34页 |
| 2.2 Semantics of νTL | 第34-35页 |
| 2.3 The Fragment G-mu | 第35-36页 |
| 2.4 νTL_f | 第36-38页 |
| 2.5 Basic Notions of Parity Games | 第38-41页 |
| 2.5.1 The Definition of Parity Games | 第38-39页 |
| 2.5.2 Strategies | 第39-40页 |
| 2.5.3 Attractor Sets | 第40-41页 |
| 2.6 Summary | 第41-43页 |
| Chapter 3 The Expressive Power of G-mu | 第43-55页 |
| 3.1 Comparison with D-mu | 第43页 |
| 3.2 Regular Expressions and ω-Regular Expressions | 第43-44页 |
| 3.2.1 Regular Expressions | 第43-44页 |
| 3.2.2 ω-Regular Expressions | 第44页 |
| 3.3 Translating ω-Regular Expressions into G-mu Formulas | 第44-53页 |
| 3.3.1 From Regular Expressions to G-mu Formulas | 第44-49页 |
| 3.3.2 From ω-Regular Expressions to G-mu Formulas | 第49-53页 |
| 3.4 Summary | 第53-55页 |
| Chapter 4 A Decision Procedure for G-mu | 第55-85页 |
| 4.1 GPF of G-mu Formulas | 第55-59页 |
| 4.1.1 GPF | 第55-57页 |
| 4.1.2 An Algorithm for Transforming G-mu Formulas into GPF | 第57-59页 |
| 4.2 Goal Progression Form Graph | 第59-64页 |
| 4.2.1 The Definition of GPG | 第59-60页 |
| 4.2.2 Marks in a GPG | 第60-62页 |
| 4.2.3 An Algorithm for Constructing GPGs | 第62-64页 |
| 4.3 A Decision Procedure Based on GPG | 第64-72页 |
| 4.3.1 ν-Paths | 第65-67页 |
| 4.3.2 The Decision Procedure | 第67-70页 |
| 4.3.3 Complexities of the Decision Procedure | 第70-72页 |
| 4.4 Model Checking Based on GPG | 第72-82页 |
| 4.4.1 Kripke Structures | 第72页 |
| 4.4.2 Product Graphs of Kripke Structures and GPGs | 第72-75页 |
| 4.4.3 ν-Paths in Product Graphs | 第75-80页 |
| 4.4.4 The GPG-Based Model Checking Algorithm | 第80页 |
| 4.4.5 Complexities of the Model Checking Algorithm | 第80-82页 |
| 4.5 Related Work | 第82-83页 |
| 4.6 Summary | 第83-85页 |
| Chapter 5 A Decision Procedure for νTL_f | 第85-101页 |
| 5.1 PFF of νTL_f Formulas | 第85-89页 |
| 5.1.1 PFF | 第85-87页 |
| 5.1.2 An Algorithm for Transforming νTL_f Formulas into PFF | 第87-89页 |
| 5.2 Present Future Form Graph | 第89-93页 |
| 5.2.1 The Definition of PFG | 第89-90页 |
| 5.2.2 An Algorithm for Constructing PFGs | 第90-93页 |
| 5.3 A Decision Procedure Based on PFG | 第93-95页 |
| 5.4 Model Checking Based on PFG | 第95-100页 |
| 5.4.1 Product Graphs of Finite Linear Structures and PFGs | 第96-97页 |
| 5.4.2 The PFG-Based Model Checking Algorithm | 第97-100页 |
| 5.5 Summary | 第100-101页 |
| Chapter 6 An Improved Recursive Algorithm for Parity Games | 第101-119页 |
| 6.1 The Recursive Algorithm for Parity Games | 第101-103页 |
| 6.2 A Preprocessing Algorithm for Parity Games | 第103-113页 |
| 6.2.1 Atomic Winning Regions | 第103-105页 |
| 6.2.2 The Preprocessing Algorithm | 第105-110页 |
| 6.2.3 Complexities of the Preprocessing Algorithm | 第110-113页 |
| 6.3 The Recursive Algorithm with an Extra Conditional Statement | 第113-116页 |
| 6.4 Related Work | 第116-117页 |
| 6.5 Summary | 第117-119页 |
| Chapter 7 Conclusions and Future Works | 第119-123页 |
| 7.1 Conclusions | 第119-120页 |
| 7.2 Future Works | 第120-123页 |
| References | 第123-137页 |
| Acknowledgements | 第137-139页 |
| Biography | 第139-141页 |
