scholarly journals Safety Verification of Interconnected Hybrid Systems Using Barrier Certificates

2016 ◽  
Vol 2016 ◽  
pp. 1-10
Author(s):  
Guobin Wang ◽  
Jifeng He ◽  
Jing Liu ◽  
Haiying Sun ◽  
Zuohua Ding ◽  
...  

Safety verification determines whether any trajectory starting from admissible initial states would intersect with a set of unsafe states. In this paper, we propose a numerical method for verifying safety of a network of interconnected hybrid dynamical systems with a state constraint based on bilinear sum-of-squares programming. The safety verification is conducted by the construction of a function of states called barrier certificate. We consider a finite number of interconnected hybrid systems satisfying the input-to-state property and the networked interconnections satisfying a dissipativity property. Through constructing a barrier certificate for each subsystem and imposing dissipation-inequality-like constraints on the interconnections, safety verification is formulated as a bilinear sum-of-squares feasibility problem. As a result, safety of the interconnected hybrid systems could be determined by solving an optimization problem, rather than solving differential equations. The proposed method makes it possible to verify the safety of interconnected hybrid systems, which is demonstrated by a numerical example.

Author(s):  
W. P. M. H. Heemels ◽  
B. De Schutter ◽  
J. Lunze ◽  
M. Lazar

Wherever continuous and discrete dynamics interact, hybrid systems arise. This is especially the case in many technological systems in which logic decision-making and embedded control actions are combined with continuous physical processes. Also for many mechanical, biological, electrical and economical systems the use of hybrid models is essential to adequately describe their behaviour. To capture the evolution of these systems, mathematical models are needed that combine in one way or another the dynamics of the continuous parts of the system with the dynamics of the logic and discrete parts. These mathematical models come in all kinds of variations, but basically consist of some form of differential or difference equations on the one hand and automata or other discrete-event models on the other hand. The collection of analysis and synthesis techniques based on these models forms the research area of hybrid systems theory, which plays an important role in the multi-disciplinary design of many technological systems that surround us. This paper presents an overview from the perspective of the control community on modelling, analysis and control design for hybrid dynamical systems and surveys the major research lines in this appealing and lively research area.


Author(s):  
Yifan Zhang ◽  
Zhengfeng Yang ◽  
Wang Lin ◽  
Huibiao Zhu ◽  
Xin Chen ◽  
...  

Author(s):  
Kazuyuki Aihara ◽  
Hideyuki Suzuki

In this introductory article, we survey the contents of this Theme Issue. This Theme Issue deals with a fertile region of hybrid dynamical systems that are characterized by the coexistence of continuous and discrete dynamics. It is now well known that there exist many hybrid dynamical systems with discontinuities such as impact, switching, friction and sliding. The first aim of this Issue is to discuss recent developments in understanding nonlinear dynamics of hybrid dynamical systems in the two main theoretical fields of dynamical systems theory and control systems theory. A combined study of the hybrid systems dynamics in the two theoretical fields might contribute to a more comprehensive understanding of hybrid dynamical systems. In addition, mathematical modelling by hybrid dynamical systems is particularly important for understanding the nonlinear dynamics of biological and medical systems as they have many discontinuities such as threshold-triggered firing in neurons, on–off switching of gene expression by a transcription factor, division in cells and certain types of chronotherapy for prostate cancer. Hence, the second aim is to discuss recent applications of hybrid dynamical systems in biology and medicine. Thus, this Issue is not only general to serve as a survey of recent progress in hybrid systems theory but also specific to introduce interesting and stimulating applications of hybrid systems in biology and medicine. As the introduction to the topics in this Theme Issue, we provide a brief history of nonlinear dynamics and mathematical modelling, different mathematical models of hybrid dynamical systems, the relationship between dynamical systems theory and control systems theory, examples of complex behaviour in a simple neuron model and its variants, applications of hybrid dynamical systems in biology and medicine as a road map of articles in this Theme Issue and future directions of hybrid systems modelling.


10.29007/7hvk ◽  
2018 ◽  
Author(s):  
Taylor T. Johnson

This report presents the results of the repeatability evaluation for a friendly competition for formal verification of continuous and hybrid systems. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, thirteen tools have been applied to solve benchmark problems for the six competition categories, of which, ten tools were evaluated and passed the repeatability evaluation. The repeatability results represent a snapshot of the current landscape of tools and the types of benchmarks for which they are particularly suited and for which others may repeat their analyses. Due to the diversity of problems in verification of continuous and hybrid systems, as well as basing on standard practice in repeatability evaluations, we evaluate the tools with pass and/or failing being repeatable. These re- sults probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems up to this date.


Author(s):  
Matthias Althoff ◽  
Goran Frehse ◽  
Antoine Girard

Reachability analysis consists in computing the set of states that are reachable by a dynamical system from all initial states and for all admissible inputs and parameters. It is a fundamental problem motivated by many applications in formal verification, controller synthesis, and estimation, to name only a few. This article focuses on a class of methods for computing a guaranteed overapproximation of the reachable set of continuous and hybrid systems, relying predominantly on set propagation; starting from the set of initial states, these techniques iteratively propagate a sequence of sets according to the system dynamics. After a review of set representation and computation, the article presents the state of the art of set propagation techniques for reachability analysis of linear, nonlinear, and hybrid systems. It ends with a discussion of successful applications of reachability analysis to real-world problems. Expected final online publication date for the Annual Review of Control, Robotics, and Autonomous Systems, Volume 4 is May 3, 2021. Please see http://www.annualreviews.org/page/journal/pubdates for revised estimates.


Author(s):  
Dan Li ◽  
Yang Wang

This research investigates the application of sum-of-squares (SOS) optimization method on finite element model updating through minimization of modal dynamic residuals. The modal dynamic residual formulation usually leads to a nonconvex polynomial optimization problem, the global optimality of which cannot be guaranteed by most off-the-shelf optimization solvers. The SOS optimization method can recast a nonconvex polynomial optimization problem into a convex semidefinite programming (SDP) problem. However, the size of the SDP problem can grow very large, sometimes with hundreds of thousands of variables. To improve the computation efficiency, this study exploits the sparsity in SOS optimization to significantly reduce the size of the SDP problem. A numerical example is provided to validate the proposed method.


2008 ◽  
Vol 2 (3) ◽  
pp. 765-772 ◽  
Author(s):  
H. Axelsson ◽  
M. Boccadoro ◽  
M. Egerstedt ◽  
P. Valigi ◽  
Y. Wardi

Author(s):  
Guobin Wang ◽  
Jing Liu ◽  
Haiying Sun ◽  
Jie Liu ◽  
Zuohua Ding ◽  
...  

Sign in / Sign up

Export Citation Format

Share Document