Symbolic Reachability Analysis of Multirate Hybrid Systems

张海宾; 段振华

您当前的位置：

首页 >

文章列表页 >

Symbolic Reachability Analysis of Multirate Hybrid Systems

更新时间：2025-12-08

- Symbolic Reachability Analysis of Multirate Hybrid Systems
- Vol. 41, Issue 4, Pages: 412-415(2007)
- 作者机构：
  
  西安电子科技大学计算理论与技术研究所,西安,710071
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP301
- Online First：10 April 2007，
  
  Published：2007
- 稿件说明：
移动端阅览
张海宾, 段振华. Symbolic Reachability Analysis of Multirate Hybrid Systems[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.

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Windage Loss and Flow Characteristics in Impeller Back Gaps of sCO2 Radial Inflow Turbines

Effects of Expansion Angle Crater Film Hole on the Film Cooling Characteristics of a Double-Wall Structure

Energy Efficiency Optimization of the Cryogenic Air Separation Process for Electronic-Grade Ultra Pure Nitrogen

Mechanism and Optimal Control Strategy for Hysteresis in Rapid Dehumidification Response of Indirect Thermal Systems in Electric Vehicles

Review of the Application of EBSILON Software in Combined Heat and Power System Optimization

Related Author

No data

Related Institution

No data

⁰