Hybrid automata is a modeling formalism for hybrid systems that results from an extension of finite-state machines by associating with each discrete state a continuous-state model. Conditions on the continuous evolution of the system invoke discrete state transitions. A broad set of analysis methods is available for hybrid automata including methods for the reachability analysis, stability analysis, and optimal control.

Definition

A hybrid automaton is a transition system that is extended with continuous dynamics. It consists of locations, transitions, invariants, guards, n-dimensional continuous functions, jump functions, and synchronization labels. Various definitions exist in the literature which differ only in details. The following definition covers all of the aspects needed for the purpose of this handbook. A hybrid automaton consists of:

• a finite set of locations Q, q ∈ Q;

• a finite transition relation ⊖ ⊆ Q × Q

for the specification of the discrete dynamics. The locations can be seen as discrete states (also called control modes), in other words as the discrete part of the hybrid state space ℋ. Transitions from one control mode to the next are often called control switches. The continuous dynamics is described by:

• a finite and indexed set of continuous variables V = {x1, x2, …, xn}, often written as a vector x = (x1, …, xn);

• a real-valued activity function f : Q × ℝn → ℝn, often defined by a continuous differential equation ẋ = dx/dt = f(q, x).

This chapter gives an informal introduction to hybrid dynamical systems and illustrates by simple examples the main phenomena that are encountered due to the interaction of continuous and discrete dynamics. References to numerous applications show the practical importance of hybrid systems theory.

What is a hybrid system?

Wherever continuous and discrete dynamics interact, hybrid systems arise. This is especially profound in many technological systems, in which logic decision making and embedded control actions are combined with continuous physical processes. 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.

Three reasons to study hybrid systems

The reasons to study hybrid systems can be quite diverse. Here we will provide three sources of motivation, which are related to (i) the design of technological systems, (ii) networked control systems, and (iii) physical processes exhibiting non-smooth behavior.

In this chapter, several applications of hybrid systems theory to benchmark process control problems are described, ranging from logic controller verification for an evaporation system to controller synthesis and optimization-based control of multiproduct batch plants and refrigerator systems.

Introduction to process control applications

While continuous feedback and feedforward control is certainly crucial for the safe, economic, and ecologically benign operation of processing plants of all kinds, the dominant part of the control software for such plants handles and generates signals and events that are discrete in nature. Logic controllers supervise and filter all inputs by the operators for their admissibility, trigger process alarms and partial or complete shut-downs, and switch between control configurations. Sequential controllers govern the start-up of devices, such as pumps and compressors, and of complete units, and the execution of batch recipes as well as shut-down sequences. Even inside continuous controllers, a lot of discrete logic is present, sensors are monitored and their signals are replaced by substitute values in case of errors, the controllers are switched between different modes, anti-windup functions are realized, etc. Exception handling is a major part of all software modules of the control system.

The correct function and economic performance of a plant thus depends on the correct interaction between a vast number of logic and discrete control functions on different layers, the continuous dynamics of the plant, and the continuous or quasicontinuous controllers.

Switched systems are described by a set of continuous state-space models together with conditions that decide which model of this set is valid for the current continuous state. As an extension of the classical linear or affine state-space representations of dynamical systems, this modelling formalism has been thoroughly investigated, as this chapter shows. The identification of the model parameters, observability, and stability analysis as well as methods for stabilization and control of switched systems are surveyed. As shown in the last section, many analysis and design problems for switched systems have a high computational complexity or are even undecidable.

Definition of the system class

Switched systems represent a type of model of hybrid systems that has been studied extensively. The reason for this research activity is given by the fact that this class of systems is very close to “non-hybrid” systems and an extension of the theory of continuous systems towards hybrid systems is, therefore, rather straightforward. Nevertheless, this system class already exhibits several important phenomena of hybrid dynamical systems.

The basic representation format is the state-space model

which describes the dynamical behavior of the system for the input u ∈ ℝm and the operation mode q ∈ Q. The vector field f and the output function g are assumed to be Lipschitz continuous with respect to x and u so that for a fixed operation mode q solutions to the state-space model exist.

Tools for mixed logical dynamical and piecewise affine systems based on the model description language HYSDEL are described. They concern various modeling, identification, analysis, control design, and verification tasks. The data exchange format explained in this chapter facilitates the combination of these tools.

This chapter describes MATLAB/Simulink tools for modeling, identifying, simulating, analyzing, and controlling discrete-time hybrid systems with piecewise affine dynamics, described in mixed logical dynamical (MLD) or piecewise affine (PWA) form. Such tools include:

• modeling and identification tools for describing the hybrid model in a high-level user-friendly way, or for identifying hybrid models from data;

• simulation tools for open-loop simulation and validation of hybrid models;

• analysis tools for characterization of stability and reachability properties of hybrid models;

• control design tools for designing hybrid model-predictive controllers, simulating closed-loop performances, and generating real-time control code.

(Section 10.1) describes the modeling language HYSDEL, which ease the process of formulating a hybrid model. Sections 10.2 and 10.3 describe two toolboxes for analysis, simulation, and control of hybrid systems, the Multi-Parametric Toolbox and the Hybrid Toolbox. (Section 10.4) describes two tools for identification of hybrid piecewise-affine models from data, the Hybrid Identification Toolbox and the PieceWise Affine Identification Toolbox. Finally, (Section 10.5) describes an interchange format for transferring models among all the aforementioned tools.

HYSDEL

Modeling aim

HYSDEL (HYbrid System DEscription Language) [632] allows modeling a class of hybrid systems described by interconnections of linear dynamical systems, finitestate automata, IF-THEN-ELSE rules, and propositional logic statements.

Automotive systems offer a rich opportunity for hybrid models, controls, and tools. Beyond the traditional use of hybrid models for representing the behavior of the composition of discrete controller and continuous plants, automotive mechanical systems exhibit hybrid behavior as demonstrated in this chapter. In addition, hybrid systems can be used to capture system specifications at the highest level of abstraction and to model implementation architectures thus enabling a rich design space exploration.

Introduction

This chapter presents an application of hybrid systems that is of significant industrial interest: power-train modeling and control for automobiles.

Engine control is a challenging problem that involves many functional and non functional requirements. The problem is to develop control algorithms and their implementation with guaranteed properties that can substantially reduce emissions and gas consumption with increased performance.

The introduction of hybrid system modeling and control was motivated by the need for verifying closed-loop systems where the plant to be controlled are continuous-time systems and the controller is a digital system. However, hybrid models are general enough to be useful in other areas of design. In particular, engine control offers a rich set of application of hybrid systems:

• The power-train itself can be represented as a hybrid system. In fact, an accurate model of a four-stroke gasoline engine has a “natural” hybrid representation:

• Each cylinder in the engine has four discrete modes of operation corresponding to the stroke it is in (hence, its behavior is well represented by a finite state machine (FSM)). […]

To facilitate an integration of tools that have been developed separately and are based on different modeling approaches, an interchange format has been developed, which is described in this chapter together with the possible tool combinations that are enabled by this format.

Overview of interchange formats for hybrid systems

The purpose of interchange formats is to establish interoperability of a wide range of tools by means of model transformations. In this way, the implementation of many bilateral translators between specific formalisms can be avoided as shown in Fig. 12.1 and 12.2.

Work on interchange formats for hybrid systems has been carried out in different projects: in the MoBIES project, the Hybrid System Interchange Format (HSIF) is defined, and in an abstract semantics of an interchange format based on the Metropolis meta model is defined (this work is a continuation of the COLUMBUS project). Finally, in the HYCON network, two interchange formats have been defined: the interchange format for switched linear systems (Section 10.5) in the form of piecewise affine systems (PWAs), and the more general compositional interchange format (CIF), which is discussed in more detail in this chapter.

In HSIF, a network of hybrid automata is used for model representation. The network behaves as a parallel composition of its automata, without hierarchy or modules. Variables can be shared or local, and the communication mechanism is based on broadcasting of Boolean “signals,” where signals are partitioned into input and output signals.

Stochastic hybrid systems involve the interaction of continuous discrete and probabilistic dynamics, and thus pose considerable conceptual, theoretical, and practical challenges. In this chapter an overview of the modeling issues that arise in the study of stochastic hybrid systems is presented. Based on this discussion, a study of the problem of reachability analysis for stochastic hybrid systems is presented.

Nondeterminism in hybrid systems

Deterministic and nondeterministic models

Much of the work on hybrid systems has focussed on deterministic models that completely characterize the future of the system without allowing any uncertainty. In practice, it is often desirable to introduce uncertainty in the models, to allow, for example, under-modeling of certain parts of the system, external unmodeled disturbances, etc. To address this need, researchers in discrete-event and hybrid systems have introduced what are known as nondeterministic models. Here the evolution is defined in a declarative way (the system specifies what solutions are allowed) as opposed to the imperative way more common in continuous dynamical/control systems (the system specifies what the solution must be).

Nondeterministic hybrid systems allow uncertainty to enter in a number of places: choice of continuous evolution (modeled, for example, by a differential inclusion), choice of discrete transition destination, or choice between continuous evolution and a discrete transition. “Choice” in this setting may reflect disturbances that add uncertainty about the system evolution, but also control inputs that can be used to steer the system evolution.

This chapter gives an overview of tools and environments for the modeling, simulation, and optimization of hybrid systems. These tasks are based on different modeling formalisms some of which have already found their way to applications.

Introduction and overview

Although the techniques and tools for the algorithmic analysis and design of hybrid systems that have been presented in the previous chapters have already been applied successfully to a variety of industrial case studies, to this day the dominant industrial tool for computer-based system analysis and design is simulation. The main reason for this lies in the large complexity of many sophisticated technological systems such as cars or chemical plants – an accurate model of a large chemical plant often consists of tens of thousands of nonlinear equations. In addition, such systems may contain hundreds of low-level continuous and logic-based controllers that ensure efficient operation or system safety, and that implement sequential procedures such as production recipes, start-up, or shut-down. For such large-scale hybrid systems, sufficiently accurate piecewise linear or affine abstractions or approximations can often not be determined, or the resulting models are too complex for the application of the techniques described above.

In the last decades, a large number of modeling and simulation tools and environments for hybrid systems have been developed, ranging from rather prototypical academic tools that mostly serve as test beds for hybrid systems research to integrated modeling and simulation environments that are capable of the real-time simulation of highly complex models with tens or even hundreds of thousands of equations using modern computing hardware.

Energy management is an issue in many applications ranging from consumer electronics to power systems. The operation of energy management systems involves many severe hybrid phenomena, mostly due to the presence of switches. As a consequence, control and optimization play a crucial role to enable increased performance and reliability, as illustrated by two examples: the control of DC-DC converters and the model-predictive supervision of the voltage stability of power networks.

Introduction to energy management

Three different categories of applications can be distinguished in the area of energy management depending on the time scale at which these systems evolve:

• Power generation involves rotating machines that are used for electricity generation and for which the physical phenomena that determine the system behavior occur in the millisecond range for the magnetic part of the machine and in the range of a second for its mechanical part.

• Power transmission is done through a network and the state of the system is characterized by the voltages at the nodes and active and reactive power flows between the nodes. Such a system typically evolves at time scales varying from seconds to minutes.

• Power conversion involves power electronics devices for which the switching frequency is typically between kilohertz and megahertz.

The first category is not considered in this chapter, the focus will be on the last two.

For specific classes of hybrid formalisms, powerful algorithms and tools for analysis and synthesis have been developed in the recent years. This chapter gives a brief overview of the functionality of tools for control design, verification, simulation, optimization, and model transformation. The tools are presented in more detail in the next chapters

In the last decade, many tools for the design and control of hybrid systems have been developed. This chapter gives an overview of some important classes of such tools. The classes are ordered according to the expressivity of the underlying mathematical model. In the end, the interconnection of tools by means of a compositional interchange format is sketched and open issues are discussed. The tools are discussed in more detail in Chapter 9–12.

Control of switched linear systems

The MATLAB/Simulink-based tools discussed in Chapter 10 are based on (deterministic) discrete-time piecewise affine (PWA) mathematical models of hybrid systems. These tools offer the following support for the design and analysis of control systems:

• Modeling: Two modeling languages with associated tools are presented: HYSDEL and MLD. HYSDEL models are based on interconnections of linear dynamical systems that are specified by means of finite-state discrete-time automata, IF-THEN-ELSE rules, and propositional logic statements. HYSDEL models can be transformed into MLD (mixed logical dynamical) models, which in turn can be transformed into discrete-time PWA models. […]

Linear hybrid automata are of interest in verification because sets of successor states can be computed exactly and efficiently using integer arithmetic. This fact is exploited in a number of formal verification algorithms that upon termination give a mathematically sound answer on whether a property holds or not. This chapter gives an overview of verification algorithms for safety properties of linear hybrid automata, and some of the over-approximation techniques that help to make the tools applicable in practice.

Formal verification and linear hybrid automata

Formal verification tries to establish with absolute certainty, in the sense of being mathematically provable, whether or not a given property is satisfied or violated by a system. In this chapter we consider algorithmic approaches to verification of safety properties such as whether a set of forbidden states is reachable. If a verification algorithm is exact (no over-approximations, no floating point computations, no rounding of any kind, etc.) and terminates, it gives the provably correct answer: safe or unsafe. Exact verification algorithms are of limited use for hybrid systems in general, since the solution of a differential equation can only be computed up to some accuracy. One may have to resort to an over-approximative algorithm, i.e. use over-approximations in the sense that when the algorithm terminates with result safe, the system really is safe. If the algorithm finds a violation, one might not know whether the violation is real or an artifact of over-approximations.