Logics for hybrid systems

被引：79
作者：
Davoren, JM [1 ]
Nerode, A
机构：
[1] Australian Natl Univ, Res Sch Informat Sci & Engn, Comp Sci Lab, Canberra, ACT, Australia
[2] Cornell Univ, Dept Math, Ithaca, NY 14853 USA
来源：
PROCEEDINGS OF THE IEEE | 2000年 / 88卷 / 07期
关键词：
automata; computer-aided analysis; computer-aided software engineering; design automation; formal languages; hybrid control systems; logic; software verification; temporal logic;
D O I：
10.1109/5.871305
中图分类号：
TM [电工技术]; TN [电子技术、通信技术];
学科分类号：
0808 ; 0809 ;
摘要：
Hybrid systems are heterogenous dynamical systems characterized by interacting continuous and discrete dynamics. Such mathematical models have proved fruitful in a great diversity of engineering applications, including air-traffic control, automated manufacturing, and chemical process control. The high-profile and safety-critical nature of the application areas has fostered a large and growing body of work on formal methods for hybrid systems: mathematical logics, computational models and methods, and computer-aided reasoning tools supporting the formal specification and verification of performance requirements for hybrid systems, and the design and synthesis of control programs for hybrid systems that are provably correct with respect to for-mat specifications. This paper offers a synthetic overview of and original contributions to, the use of logics and formal methods in the analysis of hybrid systems.
引用
收藏
页码：985 / 1010
页数：26
相关论文
共 101 条
[1]  
Akin E, 1993, GEN TOPOLOGY DYNAMIC, V1
[2]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[3]   MODEL-CHECKING IN DENSE REAL-TIME [J].
ALUR, R ;
COURCOUBETIS, C ;
DILL, D .
INFORMATION AND COMPUTATION, 1993, 104 (01) :2-34
[4]   Automatic symbolic verification of embedded systems [J].
Alur, R ;
Henzinger, TA ;
Ho, PH .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1996, 22 (03) :181-201
[5]   Alternating-time temporal logic [J].
Alur, R ;
Henzinger, TA ;
Kupferman, O .
38TH ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 1997, :100-109
[6]  
Alur R, 1997, LECT NOTES COMPUT SC, V1243, P74
[7]   THE ALGORITHMIC ANALYSIS OF HYBRID SYSTEMS [J].
ALUR, R ;
COURCOUBETIS, C ;
HALBWACHS, N ;
HENZINGER, TA ;
HO, PH ;
NICOLLIN, X ;
OLIVERO, A ;
SIFAKIS, J ;
YOVINE, S .
THEORETICAL COMPUTER SCIENCE, 1995, 138 (01) :3-34
[8]   Discrete abstractions of hybrid systems [J].
Alur, R ;
Henzinger, TA ;
Lafferriere, G ;
Pappas, GJ .
PROCEEDINGS OF THE IEEE, 2000, 88 (07) :971-984
[9]  
ALUR R, 1996, LNCS, V1066
[10]  
Alur Rajeev, 1993, Hybrid Systems, P209, DOI [DOI 10.1007/3-540-57318-6_30, DOI 10.1007/3-540-57318-6]
12345678910