Research On Formal Analysis Of Hybrid System With Segmentation

The hybrid system is a system of continuous variable dynamic systems and discrete event dynamic systems which can exchange information with each other.The dynamic characteristics of the continuous subsystems are changing constantly with the development of time.The dynamic evolution of the discrete subsystems is driven by the events.The interaction between the two systems causes the discrete trajectories to migrate on the whole and the gradual evolution on some parts.Based on the synthesis of continuous variable dynamic system and discrete time system evolution,the characteristics show more complex dynamic behavior.The formal verification of the hybrid system is one of the important research directions of the hybrid system,it analyzes whether the reachable set of the system is within the set of target states under given initial conditions.Research of the approximate analysis method of the hybrid system is studied in this paper,when targeting at getting the reachable set of the hybrid system based on the characteristics of the hybrid system,the reachable set is expressed by the polyhedron and have a good conservatism.As the calculation of the polyhedron is very complicated,with the dimension grows,the number of vertices and faces of the polyhedron grows rapidly and is difficult to deal when the system dimension is high.A new method of calculating the approximate polyhedral volume,e.g.,the segmentation method is proposed in this thesis,the paper constructs an approximate hybrid automaton based on the principle of segmentation and then solves the reachable set,the behavior equivalence of the approximate hybrid automata is analyzed finally.