\nonumchapter{Preface} \nonumsection{What are hybrid models}Mathematical models reproduce the behavior of physical phenomena.By considering the process at different levels of detail,different models of the same process are usually available inapplied sciences. Models should not be too simple, otherwise theydo not capture enough details of the process, but also not toocomplicated in order to formulate and efficiently solveinteresting analysis and synthesis problems.In the last years, several computer scientists and controltheorists have investigated models describing the interactionbetween continuous dynamics described by differential ordifference equations, and logical components described by finitestate machines, if-then-else rules, propositional and temporallogic~\cite{Ant00}. Such heterogeneous models, denoted as {\emhybrid} models, switch among many operating modes, where each modeis associated with a different dynamic law, and mode transitionsare triggered by events, like states crossing pre-specifiedthresholds.The practical relevance of hybrid models is twofold. Theincreasing profitability of logic controllers embedded in acontinuous environment is demanding for adequate modeling,analysis and design tools, for instance in the automotiveindustry~\cite{BBDPV00}. Moreover, many physical phenomena admit anatural hybrid description, like circuits integrating relays ordiodes, biomolecular networks~\cite{ABIKMPRS01}, and TCP/IPnetworks in~\cite{HBOL01}.Hybrid models are needed to address a number of problems, likedefinition and computation of trajectories, stability and safetyanalysis, control, state estimation, etc. The definition oftrajectories is usually associated with a \emph{simulator}, a toolable to compute the time evolution of the variables of the system. This may seem straightforward at first, howevermany hybrid formalisms introduce extra behaviors like Zenoeffects~\cite{joh+99zeno}, that complicate the definition oftrajectories. Although simulation allows to probe the model, itcertainly does not permit to assess structural properties of themodel. In fact any analysis based on simulation is likely to missthe subtle phenomena that a model may generate, especially in thecase of hybrid models. Tools like \emph{reachability analysis} and\emph{piecewise quadratic Lyapunov stability} are becoming astandard in analysis of hybrid systems. Reachability analysis (or\emph{safety analysis} or \emph{formal verification}) aims atdetecting if a hybrid model will eventually reach an unsafe stateconfiguration or satisfy a temporal logic formula~\cite{CES86}.Reachability analysis relies on a reach set computation algorithm,which is strongly related to the mathematical model of thesystem~\cite{SSKE01}. Piecewise quadratic Lyapunovstability~\cite{JoRa98}, is a deductive way to prove the stabilityof an equilibrium point of a subclass of hybrid systems (piecewiselinear systems), the computational burden is usually low, at theprice of a convex relaxation of the problem which leads toconservative results. While for pure linear systems it exists acomplete theory for the \emph{identification} of unknown systemparameters, the extension to general hybrid systems is still underinvestigation. {\em Controlling} a model (and therefore a process)means to choose the input such that the output tracks some desiredreference. The control (or \emph{scheduling}) problem can betackled in several ways, according to the model type and controlobjective. Most of the control approaches are based on optimalcontrol ideas (see e.g.~\cite{BBM98}). The dual problem of controlis \emph{state estimation}, which amounts to compute the value ofunmeasurable state variables based on the measurements of outputvariables. The main applicative relevance of state estimation isfor control, when direct measurements of the state vector are notpossible, and for monitoring and fault detection problems.Several classes of hybrid systems have been proposed in theliterature, each class is usually tailored to solve a particularproblem. Timed automata and hybrid automata have proved to be asuccessful modeling framework for formal verification, and havebeen widely used in the literature. The starting point for bothmodels is a finite state machine equipped with continuousdynamics. In the theory of \emph{timed automata}~\cite{ABKMPR97},the dynamic part is the continuous-time flow $\dot{x}=1$.Efficient computational tools complete the theory of timedautomata and allow to performverification~\cite{bllpww:sttt98,DOTY97} andscheduling~\cite{BFHLPRV01} of such models. Timed automata wereextended to \emph{linear hybrid automata}~\cite{ACHH93}, where thedynamics is modeled by the differential inclusion $a\leq\dot{x}\leq b$. Specific tools allow to verify such models againstsafety and liveness requirements. Linear hybrid automata werefurther extended to \emph{hybrid automata} where the continuousdynamics is governed by differential equations. Tools exist tomodel and analyze those systems, eitherdirectly~\cite{SRKC00,DM98} or by approximating the model withtimed automata or linear hybrid automata~\cite{SKPT98}.In this paper we will focus on \emph{discrete hybrid automata}(DHA). DHA result from the connection of a \emph{finite statemachine \emph{(FSM)}}, which provides the discrete part of thehybrid system, with a \emph{switched affine system \emph{(SAS)}},which provides the continuous part of the hybrid dynamics. Theinteraction between the two is based on two connecting elements:The \emph{event generator \emph{(EG)}} and the \emph{mode selector\emph{(MS)}}. The EG extracts logic signals from the continuouspart. Those logic events and other exogenous logic inputs triggerthe switch of the state of the FSM. The MS combines all the logicvariables (states, inputs, and events) to choose the mode(=continous dynamics) of the SAS. Continuous dynamics  and resetmaps are expressed as linear affine difference equations. DHAmodels are a mathematical abstraction of the features provided byother computational oriented and domain specific hybridframeworks: \emph{Mixed logical dynamical \emph{(MLD)}models}~\cite{BM99}, \emph{piecewise affine \emph{(PWA)}systems}~\cite{Son81}, \emph{linear complementarity \emph{(LC)}systems}~\cite{vdSS98,HSW00,CHS01,Hee:99,vdSS00}, \emph{extendedlinear complementarity \emph{(ELC)} systems}~\cite{dSdM99,HDB01},and \emph{max-min-plus-scaling \emph{(MMPS)}systems}~\cite{dSvdB01,HDB01}. In particular, as shown firstin~\cite{Son96} and then, with different arguments,in~\cite{HDB01,BFM00} all those modeling frameworks are equivalentand it is possible represent the same system with models of eachclass.DHA are formulated in discrete time. Despite the fact that theeffects of sampling can be neglected in most applications, subtlephenomena such as Zeno behaviors do not appear in discrete time.Although it is possible to consider hybrid automata incontinuous-time, computation is efficiently tractable only fordiscrete time models\footnote{Many tools for continuous-timehybrid models perform internally a time discretization of themodel in order to execute the computations.}. As anticipated DHAgeneralize many computational oriented models for hybrid systemsand therefore represent the starting point for solving complexanalysis and synthesis problems for hybrid systems.In particular the MLD and PWA frameworks allow to recastreachability/observability analysis, optimal control, and recedinghorizon estimation as mixed-integer linear/quadratic optimizationproblems. Reachability analysis algorithms were developedin~\cite{BTM00} for MLD and PWA hybrid systems, extendedin~\cite{BTM00c} for stability and performance analysis of hybridcontrol systems, and in~\cite{BTM01a} to perform parametricverification. In~\cite{BGT00d} the authors presented a novelapproach for solving scheduling problems using combinedreachability analysis and quadratic optimization for MLD and PWAmodels. For feedback control, in~\cite{BM99} the authors propose amodel predictive control scheme which is able to stabilize MLDsystems on desired reference trajectories while fulfillingoperating constraints, and possibly take into account previousqualitative knowledge in the form of heuristic rules. Similarly,the dual problem of state estimation admits a receding horizonsolution scheme~\cite{BeMM99a}.In \cite{vdSS98,Hee:99} (linear) complementarity systems in {\emcontinuous} time have been studied. Applications includeconstrained mechanical systems, electrical networks with idealdiodes or other dynamical systems with piecewise linear relations,variable structure systems, constrained optimal control problems,projected dynamical systems and so on~\cite[Ch.\ 2]{Hee:99}.Issues related to modeling, well-posedness (existence anduniqueness of solution trajectories), simulation anddiscretization have been of  particular interest.Finally, we mention that identification techniques for piecewiseaffine systems were recently developed~\cite{FMLM01,BRL01,JJD98},that allow to derive models (or parts of models) from input/outputdata.In this manual we present a theoretical framework for DHA systems.We will go through the steps needed for modeling a system as DHA.We will first detail the process of translating propositionallogic involving Boolean variables and linear threshold events overcontinuous variables into mixed-integer linear inequalities,generalizing several results available in theliterature~\cite{Will93,RaGr91,BM99}, in order to get anequivalent MLD form of a DHA system, which is later used to obtainthe equivalent PWA, LC, ELC, and MMPS system. We will present thetool \hysdel{} (=HYbrid Systems DEscription Language), that allowsdescribing the hybrid dynamics in a textual form, and a relatedcompiler which provides different model representations of thegiven hybrid dynamics.The latest version of the \hysdel{} compiler is available at\url{http://control.ethz.ch/~hybrid/hysdel}. Applications of\hysdel{} can be found at \url{http://control.ethz.ch/~hybrid/}.