文摘
英文文摘
声明
Chapter1 Introduction
1.1 Formal verification
1.1.1 Model Checking
1.1.2 Automated Theorem Proving
1.2 Hybrid Systems
1.3 Description of Thesis
Chapter2 Automata
2.1 Labelled Finite State Automata
2.2 Timed Automata
2.3 Hybrid Automata
2.4 Conclusion
Chapter3 Temporal Logic
3.1 Projection Temporal Logic
3.1.1 Propositional Projection Temporal Logic
3.1.2 First Order Projection Temporal Logic
3.1.3 Decidability of First Order PTL over Finite Integers
3.2 Dense Timed Interval Temporal Logic
3.2.1 Dense Timed Interval Temporal Logic
3.2.2 Decidability of Dense Timed Interval Temporal Logic
3.3 Conclusion
Chapter4 Symbolic Reachability Analysis of Hybrid Systems
4.1 Reachability Analysis of Real-Time Systems
4.1.1 Clock Zones
4.1.2 Difference Bound Matrix
4.2 Reachability Analysis of Hybrid Systems
4.2.1 Multirate Zones
4.2.2 Multirate Difference Constraint Matrix
4.2.3 Hybrid Zones
4.2.4 Difference Constraint Matrix
4.2.5 Rectangular Hybrid Diagram
4.3 Reachability Analysis of Nonlinear Hybrid Systems
4.4 Conclusion
Chapter5 Model Checking Hybrid Systems
5.1 Model Checking Multirate Hybrid Systems
5.1.1 Equivalence of Valuations
5.1.2 Region Automata
5.2 Model Checking Rectangular Hybrid Systems
5.2.1 Timed Computation Tree Logic
5.2.2 Model Checking
5.3 Conclusion
Chapter6 Hybrid Projection Temporal Logic and Theorem Proving for Hybrid Systems
6.1 Hybrid Projection Temporal Logic
6.2 Modelling of Hybrid Systems Using HPTL
6.3 An Example for Theorem Proving
6.4 Conclusion
Chapter7 Conclusions and Future Works
7.1 Conclusions
7.2 Future Works
Acknowledgements
References
Finished Papers
