REACHABILITY ANALYSIS OF DYNAMICAL-SYSTEMS HAVING PIECEWISE-CONSTANT DERIVATIVES

被引:144
作者
ASARIN, E
MALER, O
PNUELI, A
机构
[1] VERIMAG, SPECTRE, F-38330 MONTBONNOT, FRANCE
[2] MOSCOW INFORMAT TRANSMISS PROBLEMS INST, MOSCOW, RUSSIA
[3] WEIZMANN INST SCI, DEPT COMP SCI, IL-76100 REHOVOT, ISRAEL
[4] UNIV PARIS 12, VAL DE MARNE, FRANCE
基金
俄罗斯基础研究基金会;
关键词
Number:; 6021; Acronym:; -; Sponsor:; РФФИ; Sponsor: Russian Foundation for Basic Research;
D O I
10.1016/0304-3975(94)00228-B
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
In this paper we consider a class of hybrid systems, namely dynamical systems with piecewise-constant derivatives (PCD systems). Such systems consist of a partition of the Euclidean space into a finite set of polyhedral sets (regions). Within each region the dynamics is defined by a constant vector field, hence discrete transitions occur only on the boundaries between regions when the trajectories change their direction. With respect to such systems we investigate the reachability question: Given an effective description of the systems and of two polyhedral subsets P and Q of the state-space, is there a trajectory starting at some x is an element of P and reaching some point in Q? Our main results are a decision procedure for two-dimensional systems, and an undecidability result for three or more dimensions.
引用
收藏
页码:35 / 65
页数:31
相关论文
共 17 条
[1]   A THEORY OF TIMED AUTOMATA [J].
ALUR, R ;
DILL, DL .
THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235
[2]   MODEL-CHECKING IN DENSE REAL-TIME [J].
ALUR, R ;
COURCOUBETIS, C ;
DILL, D .
INFORMATION AND COMPUTATION, 1993, 104 (01) :2-34
[3]  
Alur R., 1992, LECTURE NOTES COMPUT, V736, P209, DOI DOI 10.1007/3-540-57318-6_30
[4]  
ASARIN A, 1994, LECTURE NOTES COMPUT, V820, P59
[5]   UNIVERSAL COMPUTATION AND OTHER CAPABILITIES OF HYBRID AND CONTINUOUS DYNAMICAL-SYSTEMS [J].
BRANICKY, MS .
THEORETICAL COMPUTER SCIENCE, 1995, 138 (01) :67-100
[6]  
BROCKETT RW, 1989, LECT NOTES CONTROL I, V135, P19
[7]  
BRONSTED A, 1983, INTRO CONVEX POLYTOP
[8]  
COSNARD M, 1993, LECTURE NOTES COMPUT, V665, P365
[9]   DEFINING SOFTWARE BY CONTINUOUS, SMOOTH FUNCTIONS [J].
DEMILLO, RA ;
LIPTON, RJ .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1991, 17 (04) :383-384
[10]   SYMBOLIC MODEL CHECKING FOR REAL-TIME SYSTEMS [J].
HENZINGER, TA ;
NICOLLIN, X ;
SIFAKIS, J ;
YOVINE, S .
INFORMATION AND COMPUTATION, 1994, 111 (02) :193-244