Hybrid Projection Temporal Logic and Formal Verifications of Hybrid Systems
混合投影时序逻辑与混合系统的形式化验证

To describe properties of hybrid systems, many temporal logics such as Hybrid Temporal Logic have been formalized. Although being good at describing properties of hybrid systems, these logics are not suitable for describing the behaviors of such systems. In this paper, a hybrid projection temporal logic (HPTL) is formalized. It can be used to describe both properties and implementations of hybrid systems, which enables us to do verifications of hybrid sys- tems over the same mathematical model. In addition, a set of logical equivalent formulas and an example of verifications using HPTL are given.