多速率混合系统的符号化可达性分析

张海宾; 段振华

您当前的位置：

首页 >

文章列表页 >

多速率混合系统的符号化可达性分析

专题研究 | 更新时间：2025-12-08

- 多速率混合系统的符号化可达性分析
- Symbolic Reachability Analysis of Multirate Hybrid Systems
- 西安交通大学学报 2007年41卷第4期页码：412-415
- 作者机构：
  
  西安电子科技大学计算理论与技术研究所,西安,710071
- 作者简介：
- 基金信息：
  
  : 2006-07-07. 作者简介: 张海宾(1982～),男,博士生;段振华(联系人),男,教授,博士生导师. 基金项目: 国家自然科学基金资助项目(60373103,60433010);教育部高等学校博士学科点专项科研基金资助项目(20030701015)
- DOI：
  中图分类号： TP301
- 网络首发：2007-04-10，
  
  纸质出版：2007
- 稿件说明：
移动端阅览
张海宾, 段振华. 多速率混合系统的符号化可达性分析[J]. 西安交通大学学报, 2007,41(4):412-415.

张海宾, 段振华. Symbolic Reachability Analysis of Multirate Hybrid Systems[J]. 2007, 41(4): 412-415.
张海宾, 段振华. 多速率混合系统的符号化可达性分析[J]. 西安交通大学学报, 2007,41(4):412-415. DOI：

张海宾, 段振华. Symbolic Reachability Analysis of Multirate Hybrid Systems[J]. 2007, 41(4): 412-415. DOI：

摘要

针对目前还没有专门的数据结构处理多速率混合系统的符号化可达性问题

定义了多速率区域来表示和处理多速率自动机的无穷状态空间

从而把多速率混合系统的符号化可达性分析等价地转化成多速率区域上的3种操作

即并操作、变量重赋值操作和控制状态上的时间流逝操作.从理论上证明了多速率区域在这3种操作上的封闭性

同时定义了矩阵数据结构不同上限矩阵(DCM)

并用其存储多速率区域

这样就得到了一种专门处理多速率混合系统符号化可达性分析的数据结构.理论上证得

DCM可以大大降低可达性分析算法的复杂度.

Abstract

Aiming at the problem that no special data structure has been proposed to deal with the symbolic reachability analysis of multirate hybrid systems yet

a constraint system called multirate zone is defined for the representation and manipulation of multirate automata state-spaces. A multirate zone is a conjunction of inequalities representing sets of states. Multirate zones are used as the basis for the state reachability analysis algorithm for multirate automata

which enable the algorithm to be expressed in terms of three operations in multirate zones. The operations include intersection

variable reset and elapsing of time. To present multirate zones

a matrix data structure called DCM(difference constraint matrix)is defined. Using DCM as a data structure for the reachability analysis algorithm for multirate automata

the complexity can considerably be decreased.

关键词

Keywords

references

Duan Zhenhua. Modeling of hybrid systems [D]. Western Bank,UK: Department of Computer Science, University of Shefield, 1997.

Alur R, Henzinger T A, Lafferriere G, et al. Discrete abstractions of hybrid systems [J]. Proceedings of the IEEE, 2000, 88(7):971-984.

Zhang Haibin, Duan Zhenhua. Symbolic reachability analysis of rectangular hybrid systems[C]∥The 2nd IEEE International Conference on Intelligent Computer Communication and Processing. Piscataway, USA: IEEE, 2006:240-248.

Alur R, Courcoubetis C, Henzinger T A, et al. Lecture notes in computer science 736-hybrid automata: an algorithmic approach to the specification and verification of hybrid systems [M]. London: Springer-Verlag, 1993:209-229.

Henzinger T A, Kopke P W, Puri A, et al. What's decidable about hybrid automata?[J]. Journal of Computer System Science, 1998, 57:94-124.

Dill D L. Timing assumptions and verification of finite-state concurrent systems [C]∥Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems. London:Springer-Veralg, 1989:197-212.

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

超临界水异常区域热力学特性研究

电子级超纯氮深冷空分流程节能优化研究

采用机器学习的大规模并行程序I/O性能建模与预测方法

语义区分和子图整合驱动的知识图谱表示学习方法

张角凹坑气膜孔对双层壁气膜冷却特性的影响