Approximate Formal Verification Of Hybrid Systems

Hybrid system is composed of continuous subsystem and discrete subsystem, and its two subsystems are interaction and influence each other, which makes hybrid system show a more complex dynamic behavior. One of a key content is the formal verification of system in the study of hybrid system. However, since the formal verification is very harsh, it is difficult to conduct formal verification system. In order to verify the hybrid system and to understand some of the characteristics of the hybrid system, we adopt approximate formal verification to verify the hybrid system. Thus, we mainly study the semantic model and approximate semantic model of special hybrid system and its error analysis.We study the hybrid system by means of the incomplete matrix factorization and special labels. In detail, the label is replaced by homogeneous linear polynomial differential equations. In order to obtain the preconditioner of the matrix for homogeneous linear polynomial differential equations, incomplete matrix decomposition is used. Furthermore, according to the preconditioner, equivalent label and equivalent set of labels are established. Through these two concepts, we construct approximate state of state, equivalent semantic model and approximate semantic model of labeled transition systems. By special labels, we put forward semantic models of homogeneous linear polynomial differential hybrid system. Homogeneous linear polynomial differential hybrid system not only describes the transitions between states, but also describes the details of state transition.Furthermore, approximate state trajectory, action sequence and approximate semantic model of the homogeneous linear polynomial differential hybrid system are proposed. And the approximate transition of the discrete transition is also constructed. Then, the error of the system is analyzed. Thus, we can obtain absolute errors between state and its approximate state, state trajectory reached states and its approximate state trajectory reached states,label and its approximate label, action sequence and its approximate action sequence, state trajectory and its approximate state trajectory.