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

摘要：

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

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

所属期刊栏目：34

分类号：TP3(计算技术、计算机技术)

资助基金：国家自然科学基金60373103;国家自然科学基金60433010;教育部高等学校博士学科点专项科研基金20030701015

在线出版日期：2008-01-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：279-282