Research On On Some Key Problems For Design And Verification Of Hybrid Systems

Hybrid systems are the complex dynamical systems with both discrete jumps and continuous evolutions.Many embedded systems,real-time systems and cyber physical systems can be modeled as hybrid systems.Since hybrid systems are often applied in safety-critical areas,the design and verification of hybrid systems are essential issues in both academia and industry.In practice,it always needs multiple subsystems to co-operate and interact with each other to achieve some complex control goals,which are unrealizable for an individual system.Current methods of designing such a collaborat-ing control system can hardly ensure safety and high efficiency at the same time.On the other hand,there are a lot of undetermined elements in practical situations,which makes hybrid system further evolve to stochastic systems.Current methods of veri-fying such a stochastic hybrid system cannot handle infinite time probabilistic safety verification.In this thesis,we aim to solve the design of collaborating control systems and the verification of infinite time probabilistic safety problems of stochastic hybrid systems and our work consists of three parts:the design of linear time invariant multi-agent system,the design of switched linear multi-agent system,the verification of infinite time probabilistic safety problems of stochastic hybrid systems.The main contributions of our work are as follows:?We propose a reachable set based hierarchical model predictive coordination method for discrete-time linear time invariant multi-agent systems.Current centralized ap-proaches suffer from low efficiency,while distributed approaches can hardly ensure the feasibility and stability.We point out the key problem is that the coupling among subsystems can hardly be safely decoupled.In this work,we propose a hierarchical model predictive coordination method,which basically uses reachable set to decou-ple the subsystems.In detail,the reachable set template of each subsystem should be computed in advance.At each collaboration instant,the central coordinator ob-tains the reachable sets of all the subsystems efficiently based on the current states and the reachable set templates.Then it computes the control goal of each subsys-tem at the next collaboration instant based on model predictive methodology.The control goals will then be sent to the subsystems.Once each subsystem receives the control goal,it will computed its own concrete control behavior in the next col-laboration cycle based on its dynamic model and the control goal.The experiment result shows that this approach can greatly improve the efficiency of centralized coordination methods,while still ensuring the safety.?We extend the reachable set based hierarchical model predictive coordination method to discrete-time switched linear multi-agent systems.In this work,we extend the hierarchical model predictive control to more practical cases,the collaboration of switched linear systems.Switched linear systems are a special subclass of hybrid systems,thus share some properties:the reachability is undecidable,reachable set is non-convex,and reachable set template is hard to compute.In this work,we prove that in the situation we focus,the reachability of switched linear systems is decidable,the reachable set is convex,and we also give the computation method of the reachable set template.It enables the application of hierarchical model predic-tive coordination method on the discrete-time switched linear multi-agent systems.The experiment result shows that the extended hierarchical model predictive coor-dination method is less sensitive to both the number of agents and the number of dynamic modes,compared to centralized coordination methods.?We propose a probabilistic barrier certificate method for infinite time safety veri-fication of stochastic continuous-time hybrid system.In this work,motivated by classical barrier certificate methods,we propose a barrier certificate based verifi-cation scheme for the infinite time verification of hybrid systems with initial state distribution.We also give a computational method following this scheme.In detail,we first customize the initial state set template for different initial state distribution.Then we encode the verification problem to the bilinear matrix inequation program-ming problem based on barrier certificate method.Finally,we use the BMI solver to solve the programming problem and obtain the safe initial state set,of which the probability is the lower bound of the exact safety probability.The experiment result shows that the probabilistic barrier certificate can achieve the similar safety probability with much less computation effort.