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

计算机科学 ›› 2007, Vol. 34 ›› Issue (11): 279-282.

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

张海宾段振华

西安电子科技大学计算机学院,西安710071

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
国家自然科学基金资助项目（60373103）;国家自然科学基金重大资助项目（60433010）;博士点基金资助项目（20030701015）.

ZHANG Hai-Bin ,DUAN Zhen-Hua （School of Computer Science and Technology,Xidian University,Xi＇an 710071）

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

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

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

Abstract: 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.

Key words: Hybrid systems, Hybrid automata, Interval temporal logic, Formal verification

张海宾段振华. 混合投影时序逻辑与混合系统的形式化验证[J]. 计算机科学, 2007, 34(11): 279-282. https://doi.org/

ZHANG Hai-Bin ,DUAN Zhen-Hua （School of Computer Science and Technology,Xidian University,Xi＇an 710071）. [J]. Computer Science, 2007, 34(11): 279-282. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed