| ABSTRACT | 第5-6页 |
| 摘要 | 第7-13页 |
| List of Symbols | 第13-15页 |
| List of Abbreviations | 第15-22页 |
| Chapter 1 Introduction | 第22-34页 |
| 1.1 Formal Verification | 第22-23页 |
| 1.2 Temporal Logic | 第23-25页 |
| 1.2.1 Branching-time Logic | 第23-24页 |
| 1.2.2 Linear-time Logic | 第24-25页 |
| 1.3 Temporal Logic Programming | 第25-26页 |
| 1.4 Petri Nets | 第26-30页 |
| 1.4.1 Analysis and Verification of Petri Nets | 第27-29页 |
| 1.4.2 Rapid Prototyping from Workflow Nets | 第29-30页 |
| 1.5 Contributions | 第30-32页 |
| 1.6 The Organization of the Thesis | 第32-34页 |
| Chapter 2 Preliminaries | 第34-48页 |
| 2.1 Petri Nets and Workflow Nets | 第34-36页 |
| 2.1.1 Petri Nets | 第34-36页 |
| 2.1.2 Workflow Nets | 第36页 |
| 2.2 Modeling, Simulation, and Verification Language | 第36-41页 |
| 2.2.1 Interval | 第36-37页 |
| 2.2.2 Syntax | 第37-39页 |
| 2.2.3 Operational Semantics | 第39-41页 |
| 2.3 Propositional Projection Temporal Logic | 第41-45页 |
| 2.3.1 Syntax | 第42页 |
| 2.3.2 Semantics | 第42页 |
| 2.3.3 Derived Formulas and Logical Laws | 第42-43页 |
| 2.3.4 Labeled Normal Form Graph | 第43-45页 |
| 2.4 Summary | 第45-48页 |
| Chapter 3 Model Checking of Petri Nets with MSVL | 第48-68页 |
| 3.1 Interleaving Semantics Based Translation | 第48-56页 |
| 3.2 Concurrency Semantics Based Translation | 第56-62页 |
| 3.3 Max-Concurrency Semantics Based Translation | 第62-63页 |
| 3.4 Implementation and Case Studies | 第63-65页 |
| 3.5 Summary | 第65-68页 |
| Chapter 4 PPTL Model Checking of Petri Nets | 第68-96页 |
| 4.1 PPTL Defined Over Transitions | 第68-69页 |
| 4.2 Model Checking Algorithm | 第69-74页 |
| 4.3 Termination, Completeness, and Soundness | 第74-82页 |
| 4.3.1 Termination | 第74-75页 |
| 4.3.2 Completeness | 第75-79页 |
| 4.3.3 Soundness | 第79-82页 |
| 4.4 Reduction of Petri nets | 第82-89页 |
| 4.4.1 Removing the Redundant Place | 第83-84页 |
| 4.4.2 Reducing the Choice Structure | 第84-85页 |
| 4.4.3 Reducing the Start-Choice Structure | 第85-86页 |
| 4.4.4 Reducing the End-Choice Structure | 第86-87页 |
| 4.4.5 Reducing the Concurrency Structure | 第87-89页 |
| 4.5 Implementation and Case Studies | 第89-91页 |
| 4.6 Summary | 第91-96页 |
| Chapter 5 Rapid Prototyping from Workflow Nets with MSVL | 第96-128页 |
| 5.1 Annotated Workflow Nets and Regular Structures | 第96-99页 |
| 5.1.1 Annotated Workflow Nets | 第96-97页 |
| 5.1.2 Regular Structures | 第97-99页 |
| 5.2 Structured Translation from AWFNs to MSVL Programs | 第99-113页 |
| 5.2.1 Folding the Sequence Structure | 第99-100页 |
| 5.2.2 Folding the Simple Choice Structure | 第100-101页 |
| 5.2.3 Folding the Simple Loop Structure | 第101-102页 |
| 5.2.4 Folding the Complex Loop Structure | 第102-104页 |
| 5.2.5 Folding the Complex Choice Structure | 第104-108页 |
| 5.2.6 Folding the Concurrent Structure | 第108-109页 |
| 5.2.7 Folding the Irregular Structure | 第109-113页 |
| 5.2.8 Translation Algorithm | 第113页 |
| 5.3 Soundness of the Translation | 第113-115页 |
| 5.4 Implementation and Case Studies | 第115-119页 |
| 5.4.1 A Complaints System | 第116页 |
| 5.4.2 Translation of the System | 第116-119页 |
| 5.5 Experiments | 第119-124页 |
| 5.6 Related Work | 第124-127页 |
| 5.7 Summary | 第127-128页 |
| Chapter 6 Conclusions and Future Works | 第128-132页 |
| 6.1 Conclusions | 第128-129页 |
| 6.2 Future Works | 第129-132页 |
| References | 第132-142页 |
| Acknowledgements | 第142-144页 |
| Biography | 第144-147页 |
