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

Symbolic Reachability Analysis of Multirate Hybrid Systems

针对目前还没有专门的数据结构处理多速率混合系统的符号化可达性问题,定义了多速率区域来表示和处理多速率自动机的无穷状态空间,从而把多速率混合系统的符号化可达性分析等价地转化成多速率区域上的3种操作,即并操作、变量重赋值操作和控制状态上的时间流逝操作.从理论上证明了多速率区域在这3种操作上的封闭性,同时定义了矩阵数据结构不同上限矩阵(DCM),并用其存储多速率区域,这样就得到了一种专门处理多速率混合系统符号化可达性分析的数据结构.理论上证得,DCM可以大大降低可达性分析算法的复杂度.

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.