Hybrid Systems: Computation and Control

It has been the rich body of continuous mathematics that has made possible the development of physical theories. In Newtonian mechanics, the theory of the electromagnetic field, general relativity and quantum electrodynamics, things are continuous. Were it not for the fact that things must be measured - no small consideration, of course - each theory could be formulated in a way that dispenses with numbers entirely. The rewards of continuity have been considerable. Quantum electrodynamics, is accurate to more than ten decimal places, and general relativity, under certain circumstances, accurate to more than thirteen. On the other hand, our reflections about mathematics have for more than sixty years been expressed in an entirely different language. In proof theory, model theory, recursion theory, and automata theory, things are discrete. Were it not for the fact that limits must occasionally be investigated - no small consideration, of course - each theory could be formulated in a way that dispenses with continuous functions entirely. What holds for meta-mathematics holds in a more general way for psychology. Our most sophisticated linguistic theory suggests that every human language is the expression of a unique computational system, one that is entirely discrete. What holds for linguistics is often claimed to hold for molecular biology as well; indeed, the analogies between linguistic and cellular computational systems have seemed as suggestive as they are elusive. The division of ordinary experience between material and mental objects thus finds itself mirrored in the division between continuous and discrete mathematics. In this talk, I should like to investigate the basis for the distinction, asking first whether the distinction may be expressed in terms of certain invariants, and second whether the distinction is itself an artifact, one resulting from the peculiar circumstances in which various sciences have been undertaken. I shall discuss minimalism in linguistics, the Smale-Shub theory of calculability, the use of K-theory in the evaluation of D-branes, and Stephen Wolfram's recent work in cellular automata.

Biological systems exhibit the characteristics of reactive systems remarkably, and on many levels; from the molecular, via the cellular, and all the way up to organs, full organisms, and even entire populations. Thus, a different brand of bioinformatics arises, in which, rather than “we” solving “their” computational problems, we use “our” languages, methods and tools to model and analyze “their” complex systems. This talk proposes a grand challenge for computer scientist and biologists: to model a full multi-cellular animal as a reactive system. We would like to construct a full, true-to-all-known-facts 4-dimensional model, that would be animated, flexible and comprehensive, and would enable full and realistic simulation of the animal’s development and behavior over time (the fourth dimension). It should help uncover gaps in our knowledge, correct errors, suggest new experiments and help predict unobserved phenomena. We actually have a particular organism in mind, the C. elegans nematode worm, a suggestion that is in line with the extraordinarily insightful proposal of Sydney Brenner, co-recipient of the 2002 Nobel Prize, who chose this organism 30 years ago to challenge biologists with the task of discovering the entire development and neurobiology of a living creature. The talk will argue the (long-term) feasibility of the challenge, by describing two pieces of preliminary modeling work: (i) T-cell behavior in the thymus, using statecharts with Rhapsody, linked with Flash animation, and (ii) parts of the vulval development of C. elegans, using LSCs with the Play-Engine.

Developing practical and commercially successful home robotics applications has proven to be a bigger challenge than it may seem, both technologically and commercially. During the last seven years we have gone through several product development and introduction cycles on several different platforms, including robotic lawn mowers and vacuum cleaners. In this talk I will portray our experience so far, and highlight the main lessons learned.

Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verifier performs an on-the-fly search of the finite discrete quotient whose states correspond to the truth assignments to the input predicates. To compute the transitions out of an abstract state, the tool needs to compute the set of discrete and continuous successors, and find out all the abstract states that this set intersects with. The complexity of this computation grows exponentially with the number of abstraction predicates. In this paper we present various optimizations that are aimed at speeding up the search in the abstract state-space, and demonstrate their benefits via case studies. We also discuss the completeness of the predicate abstraction technique for proving safety of hybrid systems.

In this paper we present an approach to approximate reachability computation for nonlinear continuous systems. Rather than studying a complex nonlinear system x = g(x), we study an approximating system x = f(x) which is easier to handle. The class of approximating systems we consider in this paper is piecewise linear, obtained by interpolating g over a mesh. In order to be conservative, we add a bounded input in the approximating system to account for the interpolation error. We thus develop a reachability method for systems with input, based on the relation between such systems and the corresponding autonomous systems in terms of reachable sets. This method is then extended to the approximate piecewise linear systems arising in our construction. The final result is a reachability algorithm for nonlinear continuous systems which allows to compute conservative approximations with as great degree of accuracy as desired, and more importantly, it has good convergence rate. If g is a C2 function, our method is of order 2. Furthermore, the method can be straightforwardly extended to hybrid systems.

In this paper we take the point of view that control procedures have an information theoretic content that can be more or less effectively coded. Of particular interest are control procedures for navigation and obstacle avoidance for mobile robots, and we show how tokenized instructions can be used for understanding how computer generated inputs to robotics systems should be defined, selected, and coded. To this end, a dynamic programming algorithm is developed for generating control procedures that are useful in given robotics applications.

We present a hybrid systems solution to the problem of trajectory tracking for a four-wheel steered four-wheel driven mobile robot. The robot is modelled as a non-holonomic dynamic system subject to pure rolling, no-slip constraints. Under normal driving conditions, a nonlinear trajectory tracking feedback control law based on dynamic feedback linearization is sufficient to stabilize the system and ensure asymptotically stable tracking. Transitions to other modes are derived systematically from this model, whenever the configuration space of the controlled system has some fundamental singular points. The stability of the hybrid control scheme is finally analyzed using Lyapunov-like arguments.

In this paper we show how hybrid control and modeling techniques can be put to work for solving a problem of industrial relevance in Surface Mount Technology (SMT) manufacturing. In particular, by closing the loop over the stencil printing process, we obtain a robust system that can recover from faulty initial settings, adapt to environmental changes and unscheduled interrupts, and remove discrepancies associated with bidirectional printing machines. Moreover, a timed Petri net argument is invoked for bounding the control effort in such a way that the throughput of the system is unaffected by the introduction of the closed-loop controller. The soundness of the approach is verified on a real SMT manufacturing line.

This paper describes the application of hybrid modeling and receding horizon optimal control techniques for supervising an automotive robotized gearbox, with the goal of reducing consumptions and emissions, a problem that is currently under investigation at Fiat Research Center (CRF). We show that the dynamic behavior of the vehicle can be easily approximated and captured by the hybrid model, and through simulations on standard speed patterns that a good closed loop performance can be achieved. The synthesized control law can be implemented on automotive hardware as a piecewise affine function of the measured and estimated quantities.

This paper addresses the problem of identification of piecewise affine (PWA) models. This problem involves the estimation from data of both the parameters of the affine submodels and the partition of the PWA map. The procedure that we propose for PWA identification exploits a greedy strategy for partitioning an infeasible system of linear inequalities into a minimum number of feasible subsystems: this provides an initial clustering of the datapoints. Then a refinement procedure is applied repeatedly to the estimated clusters in order to improve both the data classification and the parameter estimation. The partition of the PWA map is finally estimated by considering pairwise the clusters of regression vectors, and by finding a separating hyperplane for each of such pairs. We show that our procedure does not require to fix a priori the number of affine submodels, which is instead automatically estimated from the data.

This paper presents a Hoare-style logic for reasoning about the frequency response of control systems in the continuous-time domain. Two properties, the gain (amplitude) and phase shift, of a control system are considered. These properties are for a sinusoidal input of variable frequency. The logic operates over a simplified form of block diagram, including arbitrary transfer functions, feedback loops, and summation of signals. Reasoning is compositional, i.e. properties of a system can be deduced from properties of its subsystems. A prototype tool has been implemented in a mechanised theorem prover.

We formulate a stochastic hybrid system model that allows us to capture a class of Markov processes known as piecewise deterministic Markov processes (PDMPs). For this class of stochastic processes we formulate a probabilistic reachability problem. Basic properties of PDMPs are reviewed and used to show that the reachability question is indeed well defined. Possible methods for computing the reach probability are then concerned.

Automatic analysis of Hybrid Systems poses formidable challenges both from a modeling as well as from a verification point of view. We present a case study on automatic verification of a Turbogas Control System (TCS) using an extended version of the Mur. verifier. TCS is the heart of ICARO, a 2MW Co-generative Electric Power Plant. For large hybrid systems, as TCS is, the modeling effort accounts for a significant part of the whole verification activity. In order to ease our modeling effort we extended the Murφ verifier by importing the C language long double type (finite precision real numbers) into it.We give experimental results on running our extended Murφon our TCS model. For example using Mur. we were able to compute an admissible range of values for the variation speed of the user demand of electric power to the turbogas.

A hybrid system is proposed to model the electrical potential emitted by a neuron as a response to an externally applied DC current. Experimentally, Hodgkin and Huxley built a four-dimensional and nonlinear dynamical system to simulate this activity. Our idea is to use a new continuous and piecewise affine approximation as a hybrid model of the Hodgkin-Huxley dynamic. Our new model reproduces the Hodgkin- Huxley features with good accuracy (e.g. including the fact that the incoming current intensity is a bifurcation parameter), and, moreover, still allows an analytic computation of its solutions.

This work proposes a hybrid control methodology that integrates feedback and switching for fault-tolerant constrained control of linear parabolic partial differential equations (PDEs) for which the spectrum of the spatial differential operator can be partitioned into a finite “slow” set and an infinite stable “fast” complement. Modal decomposition techniques are initially used to derive a finite-dimensional system (set of ordinary differential equations (ODEs) in time) that captures the dominant dynamics of the PDE. The ODE system is then used as the basis for the integrated synthesis, via Lyapunov techniques, of a stabilizing nonlinear feedback controller together with a switching law that orchestrates the switching between the admissible control actuator con- figurations, based on their constrained regions of stability, in a way that respects actuator constraints and maintains closed-loop stability in the event of actuator failure. Precise conditions that guarantee stability of the constrained closed-loop PDE system under actuator switching are provided. The proposed method is applied to the problem of stabilizing an unstable, spatially unifrom steady-state of a linear parabolic PDE under constraints and actuator failures.

We consider regression problems with piecewise affine maps. In particular, we focus on the sub-problem of classifying the datapoints, i.e. correctly attributing a datapoint to the affine submodel that most likely generated it. Then, we analyze the regression algorithm proposed in [4],[3] and show that, under suitable assumptions on the dataset and the weights of the classification procedure, optimal classification can be guaranteed in presence of bounded noise. We also relax such assumptions by introducing and characterizing the property of weakly optimal classification. Finally, by elaborating on these concepts, we propose a procedure for detecting, a posteriori, misclassified datapoints.

The problem of stabilisation of a class of uncertain hybrid systems is considered. Uncertainty enters in the form of a disturbance input that can affect both the continuous and the discrete dynamics. A method for designing piecewise constant feedback controllers is developed. The controllers achieve approximate exponential convergence of the runs of the closed loop system to the zero level set of a Lyapunov function.

A hyperplane arrangement is a polyhedral cell complex where the relative position of each cell of the arrangement and the composing hyperplanes are summarized by a sign vector computable in polynomial time. This tool from computational geometry enables the development of a fast and efficient algorithm that translates the composition of hybrid systems into a piecewise affine model. The tool provides also information on the real combinatorial degree of the system which can be used to reduce the size of the search tree and the computation time of the optimization algorithms underlying optimal and model predictive control.

This paper describes the implementation of predicate abstraction techniques to automatically compute symbolic backward reachable sets of high dimensional piecewise affine hybrid automata, used to model Delta-Notch biological cell signaling networks. These automata are analyzed by creating an abstraction of the hybrid model, which is a finite state discrete transition system, and then performing the computation on the abstracted system. All the steps, from model generation to the simplification of the reachable set, have been automated using a variety of decision procedure and theorem-proving tools. The concluding example computes the reach set for a four cell network with 8 continuous and 256 discrete states. This demonstrates the feasibility of using these tools to compute on high dimensional hybrid automata, to provide deeper insight into realistic biological systems.

A modeling framework is proposed for circuits that are subject to both time and state events. The framework applies to switched networks with linear and piecewise linear elements including diodes and switches. We show that the linear complementarity formulation, which already has proved effective for piecewise linear networks, can be extended in a natural way to cover also switching circuits. We show that the proposed framework is sound in the sense that existence and uniqueness of solutions is guaranteed under a passivity assumption. We prove that only first-order impulses occur and characterize all situations that give rise to a state jump; moreover, we provide rules that determine the jump. Finally, we derive a stability result. Hence, for a subclass of hybrid dynamical systems, the issues of well-posedness, regularity of trajectories, jump rules, consistent states and stability are resolved.

The study of genetic regulatory networks has received a major impetus from the recent development of experimental techniques allowing the measurement of patterns of gene expression in a massively parallel way. This experimental progress calls for the development of appropriate computer tools for the modeling and simulation of gene regulation processes. We present a method for the hybrid modeling and simulation of genetic regulatory networks, based on a class of piecewiselinear (PL) differential equations that has been well-studied in mathematical biology. Distinguishing characteristics of the method are that it makes qualitative predictions of the behavior of regulatory systems and that it deals with discontinuities in the right-hand side of the differential equations. The simulation method has been implemented in Java in the computer tool Genetic Network Analyzer (GNA). The method and the tool have been used to analyze several networks of biological interest, including the network underlying the initiation of sporulation in Bacillus subtilis.

In this paper we investigate a new technique to determine whether an open continuous system behaves correctly for all admissible input signals. This technique is based on a discretization of the set of possible input signals, and on storing neighborhoods of points reachable by trajectories induced by those signals. Alternatively, this technique, inspired by automata theory, can be seen as an attempt to make simulation a more systematic activity by finding a small set of input signals such that the behaviors they induce “cover” the whole reachable state space.

Networked embedded systems are composed of a large number of components that interact with the physical world via a set of sensors and actuators, have their own computational capabilities, and communicate with each other via a wired or wireless network. Such systems are best modeled by distributed hybrid systems that capture the interaction between the physical and computational components. Monitoring and diagnosis of any dynamical system depend crucially on the ability to estimate the system state given the observations. Estimation for distributed hybrid systems is particularly challenging because it requires keeping track of multiple models and the transitions between them. This paper presents a particle filtering based estimation algorithm for a class of distributed hybrid systems. The hybrid estimation methodology is demonstrated on a cryogenic propulsion system.

This paper concerns the prediction of switching times for switching linear systems. The instance when a state trajectory exceeds a predefined threshold signal can be determined for input signals and time-varying thresholds without calculating the state-trajectories explicitly. This is obtained by transforming the switching conditions in the Orthogonal Function Domain of the Legendre polynomials. The problem of predicting the event time can be transposed into the problem of finding the minimal, positive and real root of a polynomial. In general, the event time can not be determined exactly, but approximated with sufficient accuracy.

This paper extends the application of the Cantor metric as a mathematical tool for defining causalities from pure discrete models to mixed-signal and hybrid models. Using the Cantor metric, which maps timed signals, continuous or discrete, into a metric space, we define causality as contractive properties of processes operating on these signals. Thus, the Banach fixed point theorem can be applies to establish conditions for the existence, uniqueness, and liveness of the behaviors for mixed-signal and hybrid systems. The results also provide theoretical foundations for the simulation technologies for such systems, including the time-marching strategy, evaluation of feedback loops, and the necessity of supporting rollback.

This paper presents an application of the Hybrid I/O Automaton (HIOA) framework [12] in verifying a realistic hybrid system. A supervisory pitch controller for a model helicopter system is designed and then verified. The design of the supervisor is limited by the actuator bandwidth, the sensor inaccuracies, and the sampling rates. Verification is carried out by induction over the length of an execution of the composed system automaton. The HIOA model makes the inductive proofs tractable by decomposing them into independent discrete and continuous parts. The paper also presents a set of language constructs for specifying hybrid I/O automata.

In this paper we propose an algorithm for solving a Multi-Object Adaptive Cruise Control problem. In a multi-object traffic scene the optimal acceleration is to be found respecting traffic rules, safety distances and driver intentions. The objective function is modelled as a quadratic cost function for the discrete time piecewise affine system. We find the optimal state-feedback control law by solving the underlying constrained finite time optimal control problem via dynamic programming.

The algorithmic analysis of timed automata is fundamentally limited by the undecidability of the universality problem. For this reason and others, there has been considerable interest in restricted classes of timed automata. In this paper we study the universality problem for two prominent such subclasses: open and closed timed automata. This problem is described as open in [6],[8] in the case of open timed automata. We show here that the problem is undecidable for open timed automata over strongly monotonic time (no two events are allowed to occur at the same time), and decidable over weakly monotonic time. For closed timed automata, we show that the problem is undecidable regardless of the monotonicity assumptions on time. As a corollary, we settle the various language inclusion problems over these classes of timed automata.

An important class of soft real-time applications require dynamic allocation of computational resources in order to comply with their quality of service (QoS) requirements. These applications are characterised by large fluctuations in their computation time requirements. One of the biggest problems in such systems is how to assign the bandwidths to the software tasks so that every task meets its QoS requirements and computational resources are not wasted.In this paper, we present a novel feedback scheduling controller based on a scheduling strategy called resource reservation. First, we model the scheduler as a discrete time switching system; then, we present hybrid control techniques for the design of the feedback scheduler; finally, we report simulation results that show the effectiveness of our approach.

This paper is concerned with the stabilizability problem for discrete-time linear systems subject to a uniform quantization of the control set and to a regular state quantization, both fixed a priori. As it is well known, for quantized systems only weak (practical) stability properties can be achieved. Therefore, we focus on the existence and construction of quantized controllers capable of steering a system to within invariant neighborhoods of the equilibrium.We first consider uniformly quantized, unbounded input sets for which an increasing family of invariant sets is constructed and quantized controllers realizing invariance are characterized. The family contains a minimal set depending only on the quantization resolution.The analysis is then extended to cases where the control set is bounded: for any given state-space set of the family above, the minimal diameter of the control set which ensures its invariance is found. The finite control set so determined also guarantees that all the states of the set can be controlled in finite time to within the family’s minimal set. It is noteworthy that the same property holds for systems without state quantization: hence, to ensure invariance and attractivity properties, the necessary control set diameter is invariant with state quantization; yet the minimal invariant set is larger. An example is .nally reported to illustrate the above results.

This paper presents the qualitative heterogeneous control framework, a methodology for the design of a controlled hybrid system based on attractors and transitions between them. This framework designs a robust controller that can accommodate bounded amounts of parametric and structural uncertainty. This framework provides a number of advantages over other similar techniques. The local models used in the design process are qualitative, allowing the use of partial knowledge about system structure, and nonlinear, allowing regions and transitions to be defined in terms of dynamical attractors. In addition, we define boundaries between local models in a natural manner, appealing to intrinsic properties of the system. We demonstrate the use of this framework by designing a novel control algorithm for the cart-pole system. In addition, we illustrate how traditional algorithms, such as linear quadratic regulators, can be incorporated within this framework. The design is validated by experiments with a physical system.

The Ö-calculus extends Milner’s π-calculus by adding active environments which flow continuously over time. This allows us to extend hybrid automata to specify systems of physical agents which can reconfigure themselves. We prove a theorem stating that processes (weakly) bisimilar in the process-algebraic sense, when placed in the same active environment, control it in the same way.

Switched circuits in power electronics by their nature present hybrid behavior. Such circuits can be described by a set of discrete states with associated continuous dynamics. A control objective, usually regulation of the output in the face of disturbances in the continuous system, is accomplished by choosing among discrete states. We describe a hybrid systems perspective of several common tasks in the design and analysis of power electronics. A DC-DC boost converter circuit is presented as an illustrative example, and the extension of this circuit to a multiple output configuration is provided to show the favorable scaling properties and broad utility of the hybrid approach.

A class of hybrid optimal control problems is formulated and a set of necessary conditions for hybrid system trajectory optimality is presented. These conditions constitute generalizations of the standard Maximum Principle (MP). Employing these conditions, we propose a class of general Hybrid Maximum Principle (HMP) based algorithms for hybrid systems optimization; these algorithms and the associated theory appear to be significantly simpler than some of the recently proposed algorithms (see [13], [14], for example). Using results from the theory of penalty function methods and Ekeland's variational principle we show the convergence of these algorithms under reasonable assumptions. The efficacy of the proposed algorithms is illustrated via several computational examples.

Computing reachable sets is an essential step in most analysis and synthesis techniques for hybrid systems. The representation of these sets has a deciding impact on the computational complexity and thus the applicability of these techniques. This paper presents a new approach for approximating reachable sets using oriented rectangular hulls (ORHs), the orientations of which are determined by singular value decompositions of sample covariance matrices for sets of reachable states. The orientations keep the over-approximation of the reachable sets small in most cases with a complexity of low polynomial order with respect to the dimension of the continuous state space. We show how the use of ORHs can improve the efficiency of reachable set computation significantly for hybrid systems with nonlinear continuous dynamics.

The use of algorithmic verification and synthesis tools for hybrid systems is currently limited to systems exhibiting simple continuous dynamics such as timed automata or rectangular hybrid systems. In this paper we enlarge the class of systems amenable to algorithmic analysis and synthesis by showing decidability of model checking Linear Temporal Logic (LTL) formulas over discrete time, controllable, linear systems. This result follows from the construction of a language equivalent, finite abstraction of a control system based on a set of finite observations which correspond to the atomic propositions appearing in a given LTL formula. Furthermore, the size of this abstraction is shown to be polynomial in the dimension of the control system and the number of observations. These results open the doors for verification and synthesis of continuous and hybrid control systems from LTL specifications.

We describe new techniques to construct, and subsequently refine, over-approximations of the reachability sets for linear dynamical systems. Our approach extracts information from real eigenvectors and more generally, from certain vectors in the primary decomposition, to generate suitable invariants of the system and can be used in conjunction with other reachability computation methods. We also describe experimental results from using this technique inside the qualitative abstraction tool [18], where it helps to generate refined abstractions of hybrid systems with linear continuous dynamics. We illustrate this on a collision-avoidance example from automobile cruise control problem, which was handled completely automatically by our tool.

We analyze the observability of the continuous and discrete states of continuous-time linear hybrid systems. For the class of jumplinear systems, we derive necessary and sufficient conditions that the structural parameters of the model must satisfy in order for filtering and smoothing algorithms to operate correctly. Our conditions are simple rank tests that exploit the geometry of the observability subspaces. For linear hybrid systems, we derive weaker rank conditions that are sufficient to guarantee the uniqueness of the reconstruction of the state trajectory, even when the individual linear systems are unobservable.

This paper surveys some of the recent progresses on computational methods for optimal control of switched systems. A general model of switched system that allows externally forced switching (EFS) and internally forced switching (IFS) is first introduced and two important classes of optimal control problems are formulated. After a brief review of some relevant theoretical results, we present the idea of two stage optimization. Based on the theoretical results and two stage optimization, we then survey computational methods based on discretization, and computational methods not based on discretization. Comments are made on the merits and restrictions of each method.