Tightened reachability constraints for the verification of linear hybrid systems

In this paper, we first generalize reachability constraints for linear differential equations, then tighten them by using the information of multiplicity of the eigenvalues and eigenvectors of such equations and put them into our constraint based approach for safety verification of hybrid systems that employs recursive reasoning to improve the method of constraint propagation based abstraction refinement.     

Hybrid systems with time scales and impulses

In this paper, we describe hybrid systems introducing special time scales and impulsive effects so as to provide a broader perspective for hybrid systems.     

Hybrid systems: Modelling and analysis using emergent dynamics

In this paper, we discuss modelling and analysis of hybrid systems with physical interaction dynamics. Such systems are typically considered complex and they are modelled using abstractions. Abstractions may, however, unintentionally exclude critical details, leading to partial or false results. Therefore, we study here use of a particle system in modelling and analysis. The novelty of the particle system is that it is designed to reveal interaction dynamics as emergent dynamics; thus, supporting analysis of complex and intricate interaction dynamics with acceptable modelling effort. As the main contribution, we formalize the particle system, and use it to model and analyze hybrid systems, both mechanical and biological, with nontrivial interaction dynamics.     

A geometric approach for reachability and observability of linear switched impulsive systems

This paper is concerned with the reachability and observability of linear switched impulsive systems with singular impulse matrices. First some new concepts with respect to the reachability and unobservability are introduced. Especially, span reachability is proposed because the reachable sets of switched impulsive systems do not always constitute subspaces. Then the geometric characterization of the span reachable and unobservable sets is presented. Moreover, the relations between the span reachable set, unobservable set and the invariant subspaces of such systems are discussed. Finally, corresponding criteria applied to linear impulsive systems and linear switched systems are also discussed.     

Canonical forms for positive discrete-time linear control systems

In this paper, the properties of reachability, controllability and essential reachability of positive discrete-time linear control systems are studied. These properties are characterized in terms of the directed graph of the state matrix. From these characterizations canonical forms of those properties are deduced.     

Hybrid port–Hamiltonian systems: From parameterized incidence matrices to hybrid automata

This paper shows how to formally design a hybrid automaton model for a wide class of dissipative physical systems with sources and switching topology. This method is based on a mathematical representation of the dynamic network graph and of its dual graph, using the hybrid incidence matrix, and on a constructive method for analyzing admissible and constrained configurations. The port–Hamiltonian representation associated with the set of hybrid system configurations, parameterized by the discrete state of the switches, is synthesized to be part of the hybrid automaton of the system. This is a further step towards a generic control synthesis for physical switching systems.     

Existence test for solution of nonlinear systems applying affine arithmetic

A computational test is proposed for existence of solution in nonlinear systems. In this test, an interval inclusion of Newton mapping is estimated applying affine arithmetic. Numerical examples are presented to show the efficiency of this test.     

A parameter estimation scheme for a class of sequential hybrid systems

It may happen that the equations governing the response of dynamical systems have some parameters whose values may not be known a priori and have to be obtained using parameter estimation schemes. In this article, we present a parameter estimation scheme for a class of sequential hybrid systems. By hybrid systems, we refer to those systems whose response is described by different governing equations corresponding to various regimes/modes of operation along with some criteria to switch between the same. In a sequential hybrid system, the different modes are arranged in a specific sequence and the system can switch from a given mode to either the previous mode or the following mode in this sequence. Here, we consider those systems whose governing equations consist of ordinary differential equations and algebraic equations. The conditions for switching between the various modes (referred to as transition conditions) are in the form of linear inequalities involving the system output. We shall first consider the case where the transition conditions are known completely. We present a parameter update scheme along with sufficient conditions that will guarantee bounded parameter estimation errors. Then, we shall consider the case where the transition conditions are not known in the sense that some parameters in these conditions are not known. We present a parameter estimation scheme for this case. We illustrate the performance of the parameter estimation scheme in both cases with some examples.     

Supervisory control of hybrid systems based on model abstraction and guided search

This paper addresses the task of computing supervisory controllers by which hybrid systems with nonlinear continuous dynamics are driven into goal sets while safety specifications are met. For this class of systems, the (conservatively approximative) determination of reachable states is an important but also a computationally expensive step of the controller synthesis. This contribution proposes a technique aiming at reducing the reach set computation by using abstract models and guided search. For a discrete abstraction of the hybrid model, candidate paths are determined as possible controlled evolutions which fulfill the given specifications. A validation scheme comprising three different techniques is applied to determine whether the candidate path represents a feasible control strategy for the hybrid system. If the specification is violated, the abstract model is refined according to the validation result. The iterative application of the determination of candidate paths, the path validation and the model refinement steers the search for a control strategy such that often only a relatively small part of the reachable state space has to be explored. The synthesis procedure is illustrated for two examples.     

A system-theoretic framework for a wide class of systems II: Input-to-output stability

In this work characterizations of the notion of Weighted Input-to-Output Stability (WIOS) for a wide class of systems with disturbances are given. Particularly, for systems with continuous dependence of the solution on the initial state and the input, the WIOS property is shown to be equivalent to robust forward completeness from the input and robust global asymptotic output stability for the corresponding input-free system.     

A New Technique for Translating Discrete Hybrid Automata into Piecewise Affine Systems

The paper proposes a new translation algorithm that translates a hybrid system described as a discrete hybrid automaton (DHA) into an equivalent piecewise affine (PWA) system. The translation algorithm exploits, among others, a new technique for cell enumeration in hyperplane arrangement, all proposed in this paper. The new translation technique enables the transfer of several analysis and synthesis tools developed for PWA systems to a DHA class of hybrid systems.     

Controllability and observability of a class of linear impulsive systems

This paper studies the controllability and observability of a class of linear piecewise constant impulsive systems. Necessary and sufficient criteria for reachability and controllability are established, respectively. It is proved that the reachability is equivalent to the controllability under some mild conditions. Then, necessary and sufficient criteria for observability and determinability of such systems are established, respectively. It is also proved that the observability is equivalent to the determinability under some mild conditions. Our criteria are of geometric type, they can be transformed into algebraic type conveniently. Finally, a numerical example is given to illustrate the utility of our criteria.     

On asymptotic optimization of a class of nonlinear stochastic hybrid systems

We consider the problem of control for continuous time stochastic hybrid systems in finite time horizon. The systems considered are nonlinear: the state evolution is a nonlinear function of both the control and the state. The control parameters change at discrete times according to an underlying controlled Markov chain which has finite state and action spaces. The objective is to design a controller which would minimize an expected nonlinear cost of the state trajectory. We show using an averaging procedure, that the above minimization problem can be approximated by the solution of some deterministic optimal control problem. This paper generalizes our previous results obtained for systems whose state evolution is linear in the control.This work is supported by the Australian Research Council. All correspondence should be directed to the first author.     

Stabilizability of a class of stochastic bilinear hybrid systems

The problem of the stabilizability of stochastic nonlinear hybrid systems with a Markovian or any switching rule is considered. Using the Lyapunov technique sufficient conditions for the asymptotic stabilizability in probability by a smooth controller in every structure are found. In particular, the asymptotic stabilizability in probability problem of stochastic bilinear hybrid systems with a Markovian or any switching rule is discussed and a closed-loop controller is found. Also the sufficient conditions for the exponential mean-square stabilizability for bilinear hybrid systems with any switching based on the Lie algebra approach are formulated and an open-loop controller is designed. The obtained results are illustrated by examples and simulations.     

Computation of continuous and piecewise affine Lyapunov functions for discrete-time systems

In this paper, we present a new approach for computing Lyapunov functions for nonlinear discrete-time systems with an asymptotically stable equilibrium at the origin. Given a suitable triangulation of a compact neighbourhood of the origin, a continuous and piecewise affine function can be parameterized by the values at the vertices of the triangulation. If these vertex values satisfy system-dependent linear inequalities, the parameterized function is a Lyapunov function for the system. We propose calculating these vertex values using constructions from two classical converse Lyapunov theorems originally due to Yoshizawa and Massera. Numerical examples are presented to illustrate the proposed approach.     

Model predictive control of nonlinear hybrid systems with discrete inputs employing a hybrid fuzzy model

The paper deals with model predictive control (MPC) of nonlinear hybrid systems with discrete inputs based on reachability analysis. In order to implement a MPC algorithm, a model of the process that we are dealing with is needed. In the paper, a hybrid fuzzy modelling approach is proposed. The hybrid system hierarchy is explained and the Takagi–Sugeno fuzzy formulation for hybrid fuzzy modelling purposes is tackled. An efficient method of identification of the hybrid fuzzy model is also discussed.

An algorithm that is–due to its MPC nature–suitable for controlling a wide spectrum of systems (provided that they have discrete inputs only) is presented.

The benefits of the algorithm employing a hybrid fuzzy model are verified on a batch reactor example. The results suggest that by suitably determining the cost function, satisfactory control can be attained, even when dealing with complex hybrid–nonlinear–stiff systems such as the batch reactor.

Finally, a comparison between MPC employing a hybrid linear model and a hybrid fuzzy model is carried out. It has been established that the latter approach clearly outperforms the approach where a linear model is used.