混合投影时序逻辑与混合系统的形式化验证

为了描述混合系统的性质和行为,10多年来,各种时序逻辑,如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范,但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑（Hybrid Projection Temporal Logic,简称HPTL）,既能刻画混合系统的性质,又能表示混合系统的实现。这样,混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时,给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。