Search

This paper introduces iterative relaxation abstraction (IRA), a new method for reachability analysis of LHA that aims to improve scalability by combining the capabilities of current tools for analysis of low-dimensional LHA with the power of linear programming (LP) for large numbers of constraints and variables. IRA is inspired by the success of counterexample guided abstraction refinement (CEGAR) techniques in verification of discrete systems. On each iteration, a low-dimensional LHA called a relaxation abstraction is constructed using a subset of the continuous variables from the original LHA. Hybrid system reachability analysis then generates a regular language called the discrete path abstraction containing all possible counterexamples (paths to the bad locations) in the relaxation abstraction. If the discrete path abstraction is non-empty, a particular counterexample is selected and LP infeasibility analysis determines if the counterexample is spurious using the constraints along the path from the original high-dimensional LHA. If the counterexample is spurious, LP techniques identify an irreducible infeasible subset (IIS) of constraints from which the set of continuous variables is selected for the the construction of the next relaxation abstraction. IRA stops if the discrete path abstraction is empty or a legitimate counterexample is found. The effectiveness of the approach is illustrated with an example. [ABSTRACT FROM AUTHOR]

This paper presents a method for computing the reach set of affine systems for sets of initial states given as low-dimensional polytopes. An affine representation for polytopes is introduced to improve the efficiency of set representations. Using the affine representation, we present a procedure to compute conservative over-approximations of the reach set, which uses the Krylov subspace approximation method to handle large-scale affine systems (systems of order over 100). [ABSTRACT FROM AUTHOR]

Results from classical dynamical systems are generalized to hybrid dynamical systems. The concept of ω limit set is introduced for hybrid systems and is used to prove new results on invariant sets and stability, where Zeno and non-Zeno hybrid systems can be treated within the same framework. As an example, LaSalle's Invariance Principle is extended to hybrid systems. Zeno hybrid systems are discussed in detail. The ω limit set of a Zeno execution is characterized for classes of hybrid systems [ABSTRACT FROM AUTHOR]

An algorithm for computing the maximal controlled invariant set and the least restrictive controller for discrete time systems is proposed. We show how the algorithm can be encoded using quantifier elimination, which leads to a semi-decidability result for definable systems. For discrete time linear systems with all sets specified by linear inequalities, a more efficient implementation is proposed using linear programming and Fourier elimination. If in addition the system is in controllable canonical form, the input is scalar and unbounded, the disturbance is scalar and bounded and the initial set is a rectangle, then the problem is decidable. [ABSTRACT FROM AUTHOR]

The main purpose of this paper is to introduce a new framework for a global, geometric study of hybrid systems, and demonstrate its usefulness through its application to the analysis of the Zeno phenomenon and stability of hybrid equilibria. [ABSTRACT FROM AUTHOR]

This paper includes an application consisting of an automatic gear-box and cruise controller which naturally is modelled as a hybrid system including state jumps in the continuous state of the controller. Motivated by this application, we extend existing stability results to include state jumps as well. The proposed stability results are based on Lyapunov techniques. The search for the (piecewise quadratic) Lyapunov functions is formulated as a linear matrix inequality (LMI) problem. It is shown how the proposed stability analysis is applied to the automatic gear-box and cruise controller. [ABSTRACT FROM AUTHOR]

A problem of great interest in the control of hybrid systems is the design of least restrictive controllers for reachability specifications. Controller design typically uses game theoretic methods which compute the region of the state space for which there exists a control such that for all disturbances, an unsafe set is not reached. In general, the computation of the controllers requires the steady state solution of a Hamilton-Jacobi-Isaacs partial differential equation which is very difficult to compute, if it exists. In this paper, we show that for classes of linear systems, the controller synthesis problem is decidable: There exists a computational algorithm which, after a finite number of steps, will exactly compute the least restrictive controller. This result is achieved by a very interesting interaction of results from mathematical logic and optimal control. [ABSTRACT FROM AUTHOR]

A special class of hybrid systems, that occurs in many applications, are the piecewise linear systems. Due to their nonlinearity, they may often be difficult to analyse. Therefore, different approximating methods have been developed for analysis, verification and control design. This paper considers one such method, and gives a method for investigating how sensitive it is to changes in the dynamics of the underlying linear subsystems. This method can be used either for robustness analysis or for control design. [ABSTRACT FROM AUTHOR]

Switching linear dynamic systems (SLDS) attempt to describe a complex nonlinear dynamic system with a succession of linear models indexed by a switching variable. Unfortunately, despite SLDS's simplicity exact state and parameter estimation are still intractable. Recently, a broad class of learning and inference algorithms for time-series models have been successfully cast in the framework of dynamic Bayesian networks (DBNs). This paper describes a novel DBN-based SLDS model. A key feature of our approach are two approximate inference techniques for overcoming the intractability of exact inference in SLDS. As an example, we apply our model to the human figure motion analysis. We present experimental results for learning figure dynamics from video data and show promising results for tracking, interpolation, synthesis, and classification using learned models. [ABSTRACT FROM AUTHOR]

We propose a computer-aided methodology to automatically generate time optimal production schemes for chemical batch plants operating in multi-batch mode. Our approach is based on the following principles: (1) the plant is modeled at the level of process operations whose behavior is specified by timed automata, (2) the optimal production schemes are generated using algorithms for reachability analysis of timed automata implemented in OpenKronos, (3) the output of the verification tool is post-processed to derive high-level control code. We apply our methodology to the batch plant at the University of Dortmund. The automatically computed operation schemes turned out to be more efficient than the previously used handwritten ones. [ABSTRACT FROM AUTHOR]

In this paper we propose a verification method for hybrid systems that is based on a successive elimination of the various system locations involved. Briefly, with each such elimination we compute a weakest precondition (strongest postcondition) on the predecessor (successor) locations such that the property to be proved cannot be violated. Experiments show that this approach is particularly interesting in cases where a standard reachability analysis would require to travel often through some of the given system locations. [ABSTRACT FROM AUTHOR]

In many cases, complex system behaviors are naturally modeled as nonlinear differential equations. However, these equations are often hard to analyze because of "stiffness" in their numerical behavior and the difficulty in generating and interpreting higher order phenomena. Engineers often reduce model complexity by transforming the nonlinear systems to piecewise linear models about operating points. Each operating point corresponds to a mode of operation, and a discrete event switching structure is added to implement the mode transitions during behavior generation. This paper presents a methodology for systematically deriving mixed continuous and discrete, i.e., hybrid models from a nonlinear ODE system model. A complete switching specification and state vector update function is derived by combining piecewise linearization with singular perturbation approaches and transient analysis. The model derivation procedure is then cast into the phase space transition ontology that we developed in earlier work. This provides a systematic mechanism for characterizing discrete transition models that result from model simplification techniques. Overall, this is a first step towards automated model reduction and simplification of complex high order nonlinear systems. [ABSTRACT FROM AUTHOR]

In this paper, we present a scheme of stochastic hybrid system which introduces randomness to the deterministic framework of the traditional hybrid systems by allowing the flow inside each invariant set of the discrete state variables to be governed by stochastic differential equation (SDE) rather than the deterministic ones. The notion of embedded Markov chains is proposed for such systems and some illustrative example from high way model is presented. As an important application, these ideas are then applied to the state space discretization of one dimensional SDE to obtain the natural discretized stochastic hybrid system together with its embedded MC. The invariant distribution and exit probability from interval of the MC are studied and it is shown that they converge to their counterparts for the solution process of the original SDE as the discretization step goes to zero. As a result, the discretized stochastic hybrid system provides a useful tool for studying various sample path properties of the SDE. [ABSTRACT FROM AUTHOR]

Reachability analysis is frequently used to study the safety of control systems. We present an implementation of an exact reachability operator for nonlinear hybrid systems. After a brief review of a previously presented algorithm for determining reachable sets and synthesizing control laws—upon whose theory the new implementation rests—an equivalent formulation is developed of the key equations governing the continuous state reachability. The new formulation is implemented using level set methods, and its effectiveness is shown by the numerical solution of three examples. [ABSTRACT FROM AUTHOR]

We define a new class of hybrid automata for which reach-ability is decidable—a proper superclass of the initialized rectangular hybrid automata—by taking parallel compositions of simple components. Attempting to generalize, we encounter timed automata with algebraic constants. We show that reachability is undecidable for these algebraic timed automata by simulating two-counter Minsky machines. Modifying the construction to apply to parametric timed automata, we reprove the undecidability of the emptiness problem, and then distinguish the dense and discrete-time cases with a new result. The algorithmic complexity—both classical and parametric—of one-clock parametric timed automata is also examined. We finish with a table of computability-theoretic complexity results, including that the existence of a Zeno run is Σ11-complete for semi-linear hybrid automata; it is too complex to be expressed in first-order arithmetic. [ABSTRACT FROM AUTHOR]

This paper reports on an on-going project to investigate techniques to diagnose complex dynamical systems that are modeled as hybrid systems. In particular, we examine continuous systems with embedded supervisory controllers that experience abrupt, partial or full failure of component devices. We cast the diagnosis problem as a model selection problem. To reduce the space of potential models under consideration, we exploit techniques from qualitative reasoning to conjecture an initial set of qualitative candidate diagnoses, which induce a smaller set of models. We refine these diagnoses using parameter estimation and model fitting techniques. As a motivating case study, we have examined the problem of diagnosing NASA's Sprint AERCam, a small spherical robotic camera unit with 12 thrusters that enable both linear and rotational motion. [ABSTRACT FROM AUTHOR]

The paper deals with the qualitative analysis of the so-called switched flow networks. Such networks are used to model various communication, computer, and flexible manufacturing systems. We prove that for any deterministic network from a specific class, there exists a finite number of limit cycles attracting all the trajectories. Furthermore, we determine this number. [ABSTRACT FROM AUTHOR]

The paper deals with the diagnosis of continuous-variable or hybrid systems whose state can be measured only by means of a quantiser. Hence, the on-line information used in the diagnosis is given by the sequences of input and output events. The paper describes how the quantised system can be represented by a semi-Markov process and how the diagnostic problem can be solved by using this timed discrete-event representation. A specific result is obtained if the model is does not include probabilistic information about the event occurrence. The diagnostic method is illustrated by considering a numerical example which concerns a part of a batch process. The results show that the temporal information included in the semi-Markov process is crucial for fault diagnosis of discrete-event systems. [ABSTRACT FROM AUTHOR]

This paper is concerned with global asymptotic stabilization of continuous-time control systems by means of quantized feedback. For linear systems, a hybrid control strategy for dealing with this problem was recently proposed by Roger Brockett and the author. The solution is based on making discrete on-line adjustments to the sensitivity of the quantizer. In the present paper we extend this method to a class of nonlinear systems. [ABSTRACT FROM AUTHOR]

This paper studies the existence of solutions to a class of hybrid automata in which the underlying continuous dynamics are rep- resented by inhomogeneous linear time-invariant systems whose inputs are controls that can be determined by the user. The principal result of the paper is a procedure that searches for global periodic non-terminating solutions of systems having a single cycle. [ABSTRACT FROM AUTHOR]

We introduce the notion of a parametrized family (Hp)p∈P of hybrid systems, and consider questions of reachability in the systems Hp as the parameter p ranges over P. Under the assumption of a uniform (as p ranges over P) finite bound on the number of discrete transitions associated to the individual systems Hp, the notion of reachability is first-order (in the sense of mathematical logic) and uniform in the parameter p. Techniques from logic can then be used to analyze computational questions associated to the family of systems. [ABSTRACT FROM AUTHOR]

This report describes the calculation of the reach sets and tubes for linear control systems with time-varying coefficients and hard bounds on the controls through tight external and internal ellipsoidal approximations. These approximating tubes touch the reach tubes from outside and inside respectively at every point of their boundary so that the surface of the reach tube is totally covered by curves that belong to the approximating tubes. The proposed approximation scheme induces a very small computational burden compared with other methods of reach set calculation. In particular such approximations may be expressed through ordinary differential equations with coefficients given in explicit analytical form. This yields exact parametric representation of reach tubes through families of external and internal ellipsoidal tubes. The proposed techniques, combined with calculation of external and internal approximations for intersections of ellipsoids, provide an approach to reachability problems for hybrid systems. [ABSTRACT FROM AUTHOR]

In this paper, we demonstrate a novel hybrid control synthesis approach using an automotive suspension system. Discrete abstractions are used to approximate the continuous dynamics and emphasis is placed on the nondeterministic nature of the abstracting models. The regulator problem for hybrid systems is formulated for safety specifications and algorithms for control design are presented. [ABSTRACT FROM AUTHOR]

We address the problem of designing a distributed, hybrid factory given a description of an assembly process and a palette of controllers for basic assembly operations. In particular, we present a method that, starting with a product assembly graph (PAG), allows us to "compile" a factory description, consisting of a geometry and a hybrid, dynamical system representing the motions of robots on that geometry. This method is based on a formalism, which we have described in previous work, that allows us to manage the details of low level, continuous control of robot actuation and high level, logical control of various couplings of robot behaviors. The factory description is intended to be an aid in the design of an actual factory, if not directly implementable itself. [ABSTRACT FROM AUTHOR]

The algorithmic approach to the analysis of timed and hybrid systems is fundamentally limited by undecidability, of universality in the timed case (where all continuous variables are clocks), and of emptiness in the rectangular case (which includes drifting clocks). Traditional proofs of undecidability encode a single Turing computation by a single timed trajectory. These proofs have nurtured the hope that the introduction of "fuzziness" into timed and hybrid models (in the sense that a system cannot distinguish between trajectories that are sufficiently similar) may lead to decidability. We show that this is not the case, by sharpening both fundamental undecidability results. Besides the obvious blow our results deal to the algorithmic method, they also prove that the standard model of timed and hybrid systems, while not "robust" in its definition of trajectory acceptance (which is affected by tiny perturbations in the timing of events), is quite robust in its mathematical properties: the undecidability barriers are not affected by reasonable perturbations of the model. [ABSTRACT FROM AUTHOR]

Since hybrid embedded systems are pervasive and often safety-critical, guarantees about their correct performance are desirable. The hybrid systems model checker HyTech provides such guarantees and has successfully verified some systems. However, HyTech severely restricts the continuous dynamics of the system being analyzed and, therefore, often forces the use of prohibitively expensive discrete and polyhedral abstractions. We have designed a new algorithm, which is capable of directly verifying hybrid systems with general continuous dynamics, such as linear and nonlinear differential equations. The new algorithm conservatively overapproximates the reachable states of a hybrid automaton by using interval numerical methods. Interval numerical methods return sets of points that enclose the true result of numerical computation and, thus, avoid distortions due to the accumulation of round-off errors. We have implemented the new algorithm in a successor tool to HyTech called HyperTech. We consider three examples: a thermostat with delay, a two-tank water system, and an air-traffic collision avoidance protocol. HyperTech enables the direct, fully automatic analysis of these systems, which is also more accurate than the use of polyhedral abstractions. [ABSTRACT FROM AUTHOR]

We consider hybrid systems consisting of a lower-level component with time-driven dynamics interacting with a higher-level component with event-driven dynamics. These typically arise in manufacturing environments where the lower-level component represents physical processes and the higher-level component represents events related to these physical processes. We formulate an optimization problem which aims at jointly optimizing the performance of both hierarchical components and present a hybrid controller for accomplishing this task. A numerical example is given to illustrate the operation of the hybrid controller. [ABSTRACT FROM AUTHOR]

We consider the synthesis of optimal controls for continuous feedback systems by recasting the problem to a hybrid optimal control problem: to synthesize optimal enabling conditions for switching between locations in which the control is constant. An algorithmic solution is obtained by translating the hybrid automaton to a finite automaton using a bisimulation and formulating a dynamic programming problem with extra conditions to ensure non-Zenoness of trajectories. We show that the discrete value function converges to the viscosity solution of the Hamilton-Jacobi-Bellman equation as a discretization parameter tends to zero. [ABSTRACT FROM AUTHOR]

In this article, we show how a behavior based control system for autonomous robots can be modeled as a hybrid automaton, where each node corresponds to a distinct robot behavior. This type of construction gives rise to chattering executions, but we show how regularized automata suggest a solution to this problem. We also discuss some design and implementation issues. [ABSTRACT FROM AUTHOR]

A general verification algorithm is described. It is then shown how ellipsoidal methods developed by A. B. Kurzhanski and P. Varaiya can be adapted to the algorithm. New numerical algorithms that compute approximations of unions of ellipsoids and intersections of ellipsoids and polyhedra were developed. The presented techniques were implemented in the verification tool called VeriSHIFT and some practical results are discussed. [ABSTRACT FROM AUTHOR]

A structural procedure is proposed for solving the problem of maximal safe-set determination based on maximal controlled invari- ant sets. However, the procedure is not guaranteed to converge in a finite number of steps. The procedure is made computationally appealing first by linearizing and discretizing the dynamical systems and, second, by using an inner approximation of these sets that, together with the classical outer approximation, yields tight bounds for an error due to the truncation of the procedure after a finite number of steps. The theory is applied to idle-speed regulation in engine control. [ABSTRACT FROM AUTHOR]

The specification for the idle control problem for automotive engines is to maintain the crankshaft speed within a given range in the presence of load changes. A new cycle-detailed hybrid model of the engine that captures well the interactions between the discrete phenomena of torque generation and spark ignition, and the continuous evolution of the power-train and air dynamics, is proposed. The idle control problem is formalized as a safety specification problem on the hybrid system. The Tomlin-Lygeros-Sastry procedure [12] is applied to compute the maximal controlled invariant set that satisfies the safety specification. [ABSTRACT FROM AUTHOR]

In this paper, we formulate the problem of characterizing the stability of a piecewise affine (PWA) system as a verification problem. The basic idea is to take the whole IRn as the set of initial conditions, and check that all the trajectories go to the origin. More precisely, we test for semi-global stability by restricting the set of initial conditions to an (arbitrarily large) bounded set X(0), and label as "asymptotically stable in T steps" the trajectories that enter an invariant set around the origin within a finite time T, or as "unstable in T steps" the trajectories which enter a set Xinst of (very large) states. Subsets of X(0) leading to none of the two previous cases are labeled as "non-classifiable in T steps". The domain of asymptotical stability in T steps is a subset of the domain of attraction of an equilibrium point, and has the practical meaning of collecting the initial conditions from which the settling time to a specified set around the origin is smaller than T. In addition, it can be computed algorithmically in finite time. Such an algorithm requires the computation of reach sets, in a similar fashion as what has been proposed for verification of hybrid systems. In this paper we present a substantial extension of the verification algorithm presented in [6] for stability characterization of PWA systems, based on linear and mixed-integer linear programming. As a result, given a set of initial conditions we are able to determine its partition into subsets of trajectories which are asymptotically stable, or unstable, or non-classifiable in T steps. [ABSTRACT FROM AUTHOR]

We propose a language, called Charon, for modular specification of interacting hybrid systems. For hierarchical description of the system architecture, Charon supports building complex agents via the operations of instantiation, hiding, and parallel composition. For hierarchical description of the behavior of atomic components, Charon supports building complex modes via the operations of instantiation, scoping, and encapsulation. Features such as weak preemption, history retention, and externally defined Java functions, facilitate the description of complex discrete behavior. Continuous behavior can be specified using differential as well as algebraic constraints, and invariants restricting the flow spaces, all of which can be declared at various levels of the hierarchy. The modular structure of the language is not merely syntactic, but can be exploited during analysis. We illustrate this aspect by presenting a scheme for modular simulation in which each mode can be compiled solely based on the locally declared information to execute its discrete and continuous updates, and furthermore, submodes can integrate at a finer time scale than the enclosing modes. [ABSTRACT FROM AUTHOR]

In this paper we describe an experimental system called d/dt for approximating reachable states for hybrid systems whose continuous dynamics is defined by linear differential equations. We use an approximation algorithm whose accumulation of errors during the continuous evolution is much smaller than in previously-used methods. The d/dt system can, so far, treat non-trivial continuous systems, hybrid systems, convex differential inclusions and controller synthesis problems. [ABSTRACT FROM AUTHOR]

Due to the persistent need to develop increasingly complex systems with improved quality and reduced development effort, automotive manufacturers are employing model-based development approaches wherever sensible. This is particularly true for powertrain control system development, as domain relevant computer-aided control system design tools have become commercially available. It is now possible to model and simulate the powertrain system dynamics in closed-loop with detailed behavioral models of the control algorithm. These control algorithm models capture nominal, initialization, diagnostic, and failure-mode-effects management modes of operation to the extent that simulation-based validation and verification procedures can be employed. These procedures help to ensure that the algorithm design and its associated software realization meet the system requirements with quality. [ABSTRACT FROM AUTHOR]

A design (at all levels of the abstraction hierarchy from functional specification to final implementation) is generally represented as a set of components, which can be considered as isolated monolithic blocks, which interact with each other and with an environment that is not part of the design. The model of computation defines the behavior and interaction of these blocks. Compactness of description, fidelity to design styles, ability to simulate, synthesize to an appropriate implementation and optimize its behavior are criteria to follow for the choice of an MOC to describe and manipulate a design. For example, some MOCs are suitable for describing complicated data transfer functions and completely unsuitable for complex control, while others are designed with complex control in mind. [ABSTRACT FROM AUTHOR]

A new generation of sensor rich, massively distributed systems is emerging that others the potential for profound economic and environmental impact, including building energy systems, deep space probes and sensor webs that monitor the earth ecosystem. These robotic webs have the richness that comes from interacting with physical environments, together with the complexity of networked software systems. They must be efficient, capable and long lived, that is, able to survive decades of autonomous operation within unforgiving environments. [ABSTRACT FROM AUTHOR]

For the past ten years, I have been designing formal specification languages for specifying software requirements on complex systems. In order to understand what is needed in such languages, my students and I have been applying our ideas to real systems and using what we have learned to generate new hypotheses about what is needed to make such languages both useful and used. This research is part of a larger effort to assist in developing safety-critical embedded systems. [ABSTRACT FROM AUTHOR]