Symbolic algorithm analysis of rectangular hybrid systems

被引：0

作者：

Zhang, Haibin ^{[1
]}

Duan, Zhenhua ^{[1
]}

机构：

[1] Xidian Univ, Inst Comp Theory & Technol, Xian, Peoples R China

来源：

THEORY AND APPLICATIONS OF MODELS OF COMPUTATION, PROCEEDINGS | 2008年 / 4978卷

关键词：

hybrid systems; model checking; temporal logic; reachability analysis;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper investigates symbolic algorithm analysis of rectangular hybrid systems. To deal with the symbolic reachability problem, a restricted constraint system called hybrid zone is formalized. Hybrid zones are also applied to a symbolic model-checking algorithm for verifying some important classes of timed computation tree logic formulas. To present hybrid zones, a data structure called difference constraint matrix is defined. Using this structure, all reachability operations and model checking algorithms for rectangular hybrid systems are implemented. These enable us to deal with the symbolic algorithm analysis of rectangular hybrid systems in an efficient way.

引用

页码：294 / 305

页数：12

共 17 条

[1] MODEL-CHECKING IN DENSE REAL-TIME
ALUR, R
COURCOUBETIS, C
DILL, D
[J]. INFORMATION AND COMPUTATION, 1993, 104 (01) : 2 - 34
[2] THE ALGORITHMIC ANALYSIS OF HYBRID SYSTEMS
ALUR, R
COURCOUBETIS, C
HALBWACHS, N
HENZINGER, TA
HO, PH
NICOLLIN, X
OLIVERO, A
SIFAKIS, J
YOVINE, S
[J]. THEORETICAL COMPUTER SCIENCE, 1995, 138 (01) : 3 - 34
[3] ALUR R, 1993, P 1993 IEEE REAL TIM
[4] ANAI H, 2001, LNCS, V2034, P63, DOI DOI 10.1007/3-540-45351-2_9
[5] ANNICHINI A, 2000, LNCS, V1855
[6] DILL DL, 1989, LECTURE NOTES COMPUT, V407, P197
[7] DUAN Z, 1997, THESIS U SHEFIELD UK
[8] What's decidable about hybrid automata?
Henzinger, TA
Kopke, PW
Puri, A
Varaiya, P
[J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1998, 57 (01) : 94 - 124
[9] HENZINGER TA, 2000, LNCS, V1785, P146
[10] A NEW POLYNOMIAL-TIME ALGORITHM FOR LINEAR-PROGRAMMING
KARMARKAR, N
[J]. COMBINATORICA, 1984, 4 (04) : 373 - 395

← 1 2 →