Hybrid models describe systems composed of both continuous and discrete components, the former typically associated with physical first principles, the latter with logic devices, such as switches, digital circuitry, software code. A typical instance are real-time systems, where physical processes are controlled by embedded controllers.
We developed a new framework for modeling hybrid systems described by interdependent linear dynamic equations, automata, and propositional logic rules, denoted as Mixed Logical Dynamical (MLD) systems. The key idea of the approach consists of embedding the logic part of the system in the dynamic equations, by transforming logic variables into 0-1 integers and by expressing the relations as mixed-integer linear inequalities. Such a translation procedure was automatized in the tool HYSDEL (HYbrid Systems DEscription Language), which generates an MLD model from a high-level textual description of the system.
Optimization-based controllers were developed for MLD models that are able to stabilize hybrid systems on desired reference trajectories while obeying operating constraints, and possibly take into account previous qualitative and heuristic knowledge about the plant operation. Due to the presence of integer variables, Mixed Integer Quadratic Programming (MIQP) optimization algorithms were investigated for implementing the proposed controllers. The potential of the method and its impact in process control were demonstrated through several case studies, including a gas supply system (Kawasaki Steel), and a combined power generation plant (ABB). For small-size/fast-sampling applications where the on-line solution of MIQP problems is computationally infeasible, we also developed algorithms for the solution of multiparametric mixed-integer linear programs, which reduce the computation burden to the simple evaluation of a piecewise linear function, as shown on a case study on traction control (Ford).
For real-time systems, a fundamental issue is to guarantee that such a combination satisfies design specifications, e.g., safety and performance requirements. Formal verification is aimed at providing such a certification: For a given set of initial conditions and disturbances, guarantee that all possible trajectories never enter a set of unsafe states, or possibly provide a counterexample. We developed a novel approach based on linear and mixed-integer linear programming for safety analysis and formal verification of hybrid systems. The effectiveness of the technique was demonstrated on a model of an automotive suspension system (Siemens) and on a batch evaporator system. Based on the tools developed for safety analysis, we also developed efficient algorithms for solving scheduling and optimal control problems for complex hybrid dynamical processes, such as those arising in manufacturing applications, and in the performance analysis of nonlinear closed-loop control systems.
Further informations:
http://control.ethz.ch /~hybrid/
