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

Hybrid Projection Temporal Logic and Formal Verifications of Hybrid Systems

作　　者：张海宾[1] 段振华[1] 

机构地区：[1]西安电子科技大学计算机学院,西安710071

出　　处：《计算机科学》2007年第11期279-282,共4页Computer Science

基　　金：国家自然科学基金(60373103);国家自然科学基金(60433010);博士点基金(20030701015)

摘　　要：为了描述混合系统的性质和行为,10多年来,各种时序逻辑,如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范,但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑(Hybrid Projection Temporal Logic,简称HPTL),既能刻画混合系统的性质,又能表示混合系统的实现。这样,混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时,给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。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 systems over the same mathematical model. In addition, a set of logical equivalent formulas and an example of verifications using HPTL are given.

关 键 词：混合系统 混合自动机 区间时序逻辑 形式化验证 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术]