| 摘要 | 第1-7页 |
| Abstract | 第7-11页 |
| 1 Introduction | 第11-21页 |
| ·Formal verification | 第11-14页 |
| ·Model Checking | 第12-13页 |
| ·Automated Theorem Proving | 第13-14页 |
| ·Hybrid Systems | 第14-18页 |
| ·Description of Thesis | 第18-21页 |
| 2 Automata | 第21-31页 |
| ·Labelled Finite State Automata | 第21-22页 |
| ·Timed Automata | 第22-24页 |
| ·Hybrid Automata | 第24-30页 |
| ·Conclusion | 第30-31页 |
| 3 Temporal Logic | 第31-51页 |
| ·Projection Temporal Logic | 第31-38页 |
| ·Propositional Projection Temporal Logic | 第31-33页 |
| ·First Order Projection Temporal Logic | 第33-35页 |
| ·Decidability of First Order PTL over Finite Integers | 第35-38页 |
| ·Dense Timed Interval Temporal Logic | 第38-49页 |
| ·Dense Timed Interval Temporal Logic | 第38-44页 |
| ·Decidability of Dense Timed Interval Temporal Logic | 第44-49页 |
| ·Conclusion | 第49-51页 |
| 4 Symbolic Reachability Analysis of Hybrid Systems | 第51-85页 |
| ·Reachability Analysis of Real-Time Systems | 第52-56页 |
| ·Clock Zones | 第52-55页 |
| ·Difference Bound Matrix | 第55-56页 |
| ·Reachability Analysis of Hybrid Systems | 第56-79页 |
| ·Multirate Zones | 第56-60页 |
| ·Multirate Difference Constraint Matrix | 第60-64页 |
| ·Hybrid Zones | 第64-72页 |
| ·Difference Constraint Matrix | 第72-76页 |
| ·Rectangular Hybrid Diagram | 第76-79页 |
| ·Reachability Analysis of Nonlinear Hybrid Systems | 第79-83页 |
| ·Conclusion | 第83-85页 |
| 5 Model Checking Hybrid Systems | 第85-99页 |
| ·Model Checking Multirate Hybrid Systems | 第85-95页 |
| ·Equivalence of Valuations | 第86-90页 |
| ·Region Automata | 第90-95页 |
| ·Model Checking Rectangular Hybrid Systems | 第95-98页 |
| ·Timed Computation Tree Logic | 第95-96页 |
| ·Model Checking | 第96-98页 |
| ·Conclusion | 第98-99页 |
| 6 Hybrid Projection Temporal Logic and Theorem Proving for Hybrid Systems | 第99-109页 |
| ·Hybrid Projection Temporal Logic | 第99-104页 |
| ·Modelling of Hybrid Systems Using HPTL | 第104-106页 |
| ·An Example for Theorem Proving | 第106-107页 |
| ·Conclusion | 第107-109页 |
| 7 Conclusions and Future Works | 第109-111页 |
| ·Conclusions | 第109-110页 |
| ·Future Works | 第110-111页 |
| Acknowledgements | 第111-113页 |
| References | 第113-121页 |
| Finished Papers | 第121页 |
