Search

This paper discusses the problems of control design and stability analysis of the networked control systems(NCSs) with random delays. The network-induced delays of the NCS are considered as interval variables governed by a Markov chain. Using the upper and lower bounds of the delays, a discrete-time Markovian jump system with norm-bounded uncertainties is presented to model the NCS. Based on this model, a state feedback controller can be constructed via a set of linear matrix inequalities. Simulations are given to illustrate the proposed results. [ABSTRACT FROM AUTHOR]

In this paper we demonstrate how to construct barrier certificates for safety verification of nonlinear hybrid systems using sum of squares methodologies, with particular emphasis on the computational challenges of the technique when applied to an Advanced Life Support System. The controlled system aims to ensure that the carbon dioxide and oxygen concentrations in a Variable Configuration CO2 Removal (VCCR) subsystem never reach unacceptable values. The model we use is in the form of a hybrid automaton consisting of six modes each with nonlinear continuous dynamics of state dimension 10. The sheer size of the system makes the task of safety verification difficult to tackle with any other methodology. This is the first application of the sum of squares techniques to the safety verification of an intrinsically hybrid system with such high dimensional continuous dynamics. [ABSTRACT FROM AUTHOR]

A switched linear system is said to be controllable, if for any given initial state and terminal state, one can find a switching sequence and corresponding input such that the system can be driven from the initial state to the terminal state. Necessary and sufficient condition on the controllability of switched linear systems has been established, and a single switching sequence can be constructed to realize the controllability. In this paper, the stabilizability problem for switched linear systems is formulated and we show that controllability implies stabilizability for switched linear systems. In our framework, we using periodically switching sequence and piecewise constant feedback controller. Two stabilization design methods, the pole assignment method and the linear matrix inequality method are proposed. Furthermore, if a switched linear system is both controllable and observable, then an observer-based output feedback controller can be constructed when the system state is not available. In this case, the well-known Separation Principle is shown to still hold. All these results are built upon our previously established fundamental geometric properties of controllability realization as well as the important fact that both controllability and observability can be realized through a single switching sequence. [ABSTRACT FROM AUTHOR]

We present a method for the computation of reachable sets of uncertain linear systems. The main innovation of the method consists in the use of zonotopes for reachable set representation. Zonotopes are special polytopes with several interesting properties : they can be encoded efficiently, they are closed under linear transformations and Minkowski sum. The resulting method has been used to treat several examples and has shown great performances for high dimensional systems. An extension of the method for the verification of piecewise linear hybrid systems is proposed. [ABSTRACT FROM AUTHOR]

In this paper we consider the problem of developing sensor/actuator abstractions for embedded control design. These abstractions take the form of inequalities relating sensor/actuator characteristics with the continuous dynamics' output. When satisfied, they allow to decouple control design from the choice of sensor/actuators, thus simplifying control design while ensuring implementability. [ABSTRACT FROM AUTHOR]

Modeling and analysis techniques are presented for real-time, safety-critical software. Software analysis is the task of verifying whether the computer code will execute safely, free of run-time errors. The critical properties that prove safe execution include bounded-ness of variables and termination of the program in finite time. In this paper, dynamical system representations of computer programs along with specific models that are pertinent to analysis via an optimization-based search for system invariants are developed. It is shown that the automatic search for system invariants that establish the desired properties of computer code, can be formulated as a convex optimization problem, such as linear programming, semidefinite programming, and/or sum of squares programming. [ABSTRACT FROM AUTHOR]

CPDPs (Communicating Piecewise Deterministic Markov Processes) can be used for compositional specification of systems from the class of stochastic hybrid processes formed by PDPs (Piecewise Deterministic Markov Processes). We define CPDPs and the composition of CPDPs, and prove that the class of CPDPs is closed under composition. Then we introduce a notion of bisimulation for PDPs and CPDPs and we prove that bisimilar PDPs as well as bisimilar CPDPs have equal stochastic behavior. Finally, as main result, we prove the congruence property that, for a composite CPDP, substituting components by different but bisimilar components results in a CPDP that is bisimilar to the original composite CPDP (and therefore has equal stochastic behavior). [ABSTRACT FROM AUTHOR]

This paper deals with the problem of safety verification of non-linear hybrid systems. We start from a classical method that uses interval arithmetic to check whether trajectories can move over the boundaries in a rectangular grid. We put this method into an abstraction refinement framework and improve it by developing an additional refinement step that employs constraint propagation to add information to the abstraction without introducing new grid elements. Moreover, the resulting method allows switching conditions, initial states and unsafe states to be described by complex constraints instead of sets that correspond to grid elements. Nevertheless, the method can be easily implemented since it is based on a well-defined set of constraints, on which one can run any constraint propagation based solver. First tests of such an implementation are promising. [ABSTRACT FROM AUTHOR]

In 1995, HyTech broke new ground as a potentially powerful tool for verifying hybrid systems - yet it has remained severely limited in its applicability to more complex systems. We address the main problems of HyTech with PHAVer, a new tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives. Affine dynamics are handled by on-the-fly overapproximation and by partitioning the state space based on user-definable constraints and the dynamics of the system. PHAVer's exact arithmetic is robust due to the use of the Parma Polyhedra Library, which supports arbitrarily large numbers. To manage the complexity of the polyhedral computations, we propose methods to conservatively limit the number of bits and constraints of polyhedra. Experimental results for a navigation benchmark and a tunnel diode circuit show the effectiveness of the approach. [ABSTRACT FROM AUTHOR]

We present a powerful computational method for automatically generating polynomial invariants of hybrid systems with linear continuous dynamics. When restricted to linear continuous dynamical systems, our method generates a set of polynomial equations (algebraic set) that is the best such over-approximation of the reach set. This shows that the set of algebraic invariants of a linear system is computable. The extension to hybrid systems is achieved using the abstract interpretation framework over the lattice defined by algebraic sets. Algebraic sets are represented using canonical Gröbner bases and the lattice operations are effectively computed via appropriate Gröbner basis manipulations. [ABSTRACT FROM AUTHOR]

In this paper, we present a new approach to the Direct Torque Control (DTC) problem of three-phase induction motor drives. This approach is based on Model Predictive Control (MPC) exploiting the specific structure of the DTC problem and using a systematic design procedure. Specifically, by observing that the DTC objectives, which require the controlled variables to remain within certain bounds, are related to feasibility rather than optimality, and by using a blocking control inputs regime for the whole prediction horizon we derive a low complexity controller. The derived controller is an explicit state-feedback control law that can be implemented as a look-up table. Even though the controller is derived here for a DTC drive featuring a two-level inverter, the control scheme can be extended to also tackle three-level inverters. Simulation results demonstrate that the proposed controller leads to performance improvements despite its simple structure. [ABSTRACT FROM AUTHOR]

In this paper, we study the problem of controlling the expected exit time from a region for a class of stochastic hybrid systems. That is, we find the least costly feedback control for a stochastic hybrid system that can keep its state inside a prescribed region for at least an expected amount of time. The stochastic hybrid systems considered are quite general: the continuous dynamics are governed by stochastic differential equations, and the discrete mode evolves according to a continuous time Markov chain. Instead of adopting the usual Hamilton-Jacobi viewpoint, we study the problem directly by formulating it as a PDE constrained optimization problem, and propose a solution using adjoint-based gradient descent methods. Numerical results of the proposed approach are presented for several representative examples, and, for the simple case, compared with analytical results. [ABSTRACT FROM AUTHOR]

Interchange formats have been the backbone of the EDA industry for several years. They are used as a way of helping the development of design flows that integrate foreign tools using formats with different syntax and, more importantly, different semantics. The need for integrating tools coming from different communities is even more severe for hybrid systems because of the relative immaturity of the field and the intrinsic difficulty of the mathematical underpinnings. In this paper, we provide a discussion about interchange formats for hybrid systems, we survey the approaches used by different tools for analysis (simulation and formal verification) and synthesis of hybrid systems, and we give a recommendation for an interchange format for hybrid systems based on the Metropolis metamodel. The proposed interchange format has rigorous semantics and can accommodate the translation to and from the formats of the tools we have surveyed while providing a formal reasoning framework. [ABSTRACT FROM AUTHOR]

A methodology for safety verification using barrier certificates has been proposed recently. Conditions that must be satisfied by a barrier certificate can be formulated as a convex program, and the feasibility of the program implies system safety, in the sense that there is no trajectory starting from a given set of initial states that reaches a given unsafe region. The dual of this problem, i.e., the reachability problem, concerns proving the existence of a trajectory starting from the initial set that reaches another given set. Using insights from convex duality and the concept of density functions, in this paper we show that reachability can also be verified through convex programming. Several convex programs for verifying safety, reachability, and other properties such as eventuality are formulated. Some examples are provided to illustrate their applications. [ABSTRACT FROM AUTHOR]

This paper demonstrates the use of a hybrid system approach to design optimal controllers for smart damping materials. Recently, controllers have been used to switch piezoelectric materials for mechanical vibration suppression. These controllers allow a small implementation and require little or no power. However, the control laws to switch these circuits are derived heuristically and it remains unclear, if better control laws exist. We present a new control approach based on a hybrid system framework. This allows to derive optimal switching laws by solving a receding horizon optimal control problem with multi-parametric programming. Additionally, we show how to implement the optimal switching laws with analog electronic circuitry such that the resulting damping circuits do not require power for operation. Simulations show the improvement of the damping compared with heuristically derived circuits and experiments demonstrate that the autonomous damping circuits can suppress vibration without requiring additional power. [ABSTRACT FROM AUTHOR]

Motivated by three applications which are under investigation at the Honeywell Research Laboratory in Minneapolis, we introduce a class of large scale control problems. In particular we show that a formation flight problem, a paper machine control problem and the coordination of cameras in a monitoring network can be cast into this class. In the second part of the paper we propose a decentralized control scheme to tackle the complexity of the problem. The scheme makes use of logic rules which improve stability and feasibility of the decentralized method by enforcing coordination. The decentralized control laws which respect the rules are computed using hybrid control design. [ABSTRACT FROM AUTHOR]

In this paper, we propose a new method to deal with hybrid systems based on the concept of the nonstandard analysis and the Büchi's transfinite automata. An essential point of the method is a generalization of hybrid automata with hyperfinite iteration of an infinitesimal transition in . This nonstandard model of hybrid automata allows discrete but hyperfinite state transition, so that we can describe and reason about the interaction of the continuous and discrete dynamics in the algebraic framework. In this enlarged perspective of the hybrid automata, we discuss about the asymptotic orbit of the dynamics that is peculiar to the hybrid systems such as Zeno. [ABSTRACT FROM AUTHOR]

Hamilton-Jacobi partial differential equations have many applications in the analysis of nondeterministic continuous and hybrid systems. Unfortunately, analytic solutions are seldom available and numerical approximation requires a great deal of programming infrastructure. In this paper we describe the first publicly available toolbox for approximating the solution of such equations, and discuss three examples of how these equations can be used in system analysis: cost to go, stochastic differential games, and stochastic hybrid systems. For each example we briefly summarize the relevant theory, describe the toolbox implementation, and provide results. [ABSTRACT FROM AUTHOR]

Multi-modal control is a commonly used design tool for breaking up complex control tasks into sequences of simpler tasks. In this paper, we show that by viewing the control space as a set of such tokenized instructions rather than as real-valued signals, reinforcement learning becomes applicable to continuous-time control systems. In fact, we show how a combination of state-space exploration and multi-modal control converts the original system into a finite state machine, on which Q-learning can be utilized. [ABSTRACT FROM AUTHOR]

We present a closed-form (linear-algebraic) solution to the identification of deterministic switched ARX systems and characterize conditions that guarantee the uniqueness of the solution. We show that the simultaneous identification of the number of ARX systems, the (possibly different) model orders, the ARX model parameters, and the switching sequence is equivalent to the identification and decomposition of a projective algebraic variety whose degree and dimension depend on the number of ARX systems and the model orders, respectively. Given an upper bound for the number of systems, our algorithm identifies the variety and the maximum orders by fitting a polynomial to the data, and the number of systems, the model parameters, and the switching sequence by differentiating this polynomial. Our method is provably correct in the deterministic case, provides a good sub-optimal solution in the stochastic case, and can handle large low-dimensional data sets (up to tens of thousands points) in a batch fashion. [ABSTRACT FROM AUTHOR]

In this contribution we consider the approach to the runway as a case study of our research on conflict resolution for Air-Traffic Control with stochastic models. We simulate the approach for landing and optimise the maneuver through a simulation based optimisation strategy. [ABSTRACT FROM AUTHOR]

In this paper we develop a priori stabilization conditions for infinity norm based hybrid MPC in the terminal cost and constraint set fashion. Closed-loop stability is achieved using infinity norm inequalities that guarantee that the value function corresponding to the MPC cost is a Lyapunov function of the controlled system. We show that Lyapunov asymptotic stability can be achieved even though the MPC value function may be discontinuous. One of the advantages of this hybrid MPC scheme is that the terminal constraint set can be directly obtained as a sublevel set of the calculated terminal cost, which is also a local piecewise linear Lyapunov function. This yields a new method to obtain positively invariant sets for PWA systems. [ABSTRACT FROM AUTHOR]

We propose a new approximation technique for Hybrid Automata. Given any Hybrid Automaton H, we call Approx(H,k) the Polynomial Hybrid Automaton obtained by approximating each formula φ in H with the formulae φk obtained by replacing the functions in φ with their Taylor polynomial of degree k. We prove that Approx(H,k) is an over-approximation of H. We study the conditions ensuring that, given any ε > 0, some k0 exists such that, for all k>k0, the "distance" between any vector satisfying φk and at least one vector satisfying φ is less than ε. We study also conditions ensuring that, given any ε > 0, some k0 exists such that, for all k > k0, the "distance" between any configuration reached by Approx(H,k) in n steps and at least one configuration reached by H in n steps is less than ε. [ABSTRACT FROM AUTHOR]

In this paper, we present a new design methodology for synchronous reactive systems, based on a clear separation between control and data flow parts. This methodology allows to facilitate the specification of different kinds of systems and to have a better readability. It also permits to separate the study of the different parts by using the most appropriate existing tools for each of them. Following this idea, we are particularly interested in the notion of running modes and in the Scade tool. Scade is a graphical development environment coupling data processing and state machines (modeled by the synchronous languages Lustre and Esterel). It can be used to specify, simulate, verify and generate C code. However, this tool does not follow any design methodology, which often makes difficult the understanding and the re-use of existing applications. We will show that it is also difficult to separate control and data flow parts using Scade. Regulation systems are better specified using mode-automata which allow adding an automaton structure to data flow specifications written in Lustre. When we observe the mode-structure of the mode-automaton, we clearly see where the modes differ and the conditions for changing modes. This makes it possible to better understand the behavior of the system. In this work, we try to combine the advantages of Scade and running modes, in order to develop a new design methodology which facilitates the study of several systems by respecting the separation between control and data flows. This schema is illustrated through the Climate case study suggested by Esterel Technologieswww.esterel-technologies.com, in order to exhibit the benefits of our approch compared to the one advocated in Scade. [ABSTRACT FROM AUTHOR]

This paper presents an ontology-based approach to heterogeneous verification of embedded systems, that is, the integration of verification results from different tools and different models of embedded system applications. We present an overview of our proposed framework and explain the key components. We then describe an initial ontology for embedded control applications and its mapping to a knowledge base. We illustrate this initial framework using an example of an automotive power window controller. The concluding discussion describes our current work and future research directions. Keywords: ontology, knowledge base, knowledge integration, theorem proving. [ABSTRACT FROM AUTHOR]

In this paper we compare four recently proposed procedures for the identification of PieceWise AutoRegressive eXogenous (PWARX) and switched ARX models. We consider the clustering-based procedure, the bounded-error procedure, and the Bayesian procedure which all identify PWARX models. We also study the algebraic procedure, which identifies switched linear models. We introduce quantitative measures for assessing the quality of the obtained models. Specific behaviors of the procedures are pointed out, using suitably constructed one dimensional examples. The methods are also applied to the experimental identification of the electronic component placement process in pick-and-place machines. [ABSTRACT FROM AUTHOR]

Under standard Lipschitz conditions, trajectories of systems described by ordinary differential equations are well defined in both forward and reverse time. (The flow map is invertible.) However for hybrid systems, uniqueness of trajectories in forward time does not guarantee flow-map invertibility, allowing non-uniqueness in reverse time. The paper establishes a necessary and sufficient condition that governs invertibility through events. It is shown that this condition is equivalent to requiring reverse-time trajectories to transversally encounter event triggering hypersurfaces. This analysis motivates a homotopy algorithm that traces a one-manifold of initial conditions that give rise to trajectories which all reach a common point at the same time. [ABSTRACT FROM AUTHOR]

This paper deals with polynomial stochastic hybrid systems (pSHSs), which generally correspond to stochastic hybrid systems with polynomial continuous vector fields, reset maps, and transition intensities. For pSHSs, the dynamics of the statistical moments of the continuous states evolve according to infinite-dimensional linear ordinary differential equations (ODEs). We show that these ODEs can be approximated by finite-dimensional nonlinear ODEs with arbitrary precision. Based on this result, we provide a procedure to build this type of approximations for certain classes of pSHSs. We apply this procedure for several examples of pSHSs and evaluate the accuracy of the results obtained through comparisons with Monte Carlo simulations. These examples include: the modeling of TCP congestion control both for long-lived and on-off flows; state-estimation for networked control systems; and the stochastic modeling of chemical reactions. [ABSTRACT FROM AUTHOR]

Counterexample guided abstraction refinement, a powerful technique for verifying properties of discrete-state systems, has been extended recently to hybrid systems verification. Unlike in discrete systems, however, establishing the successor relation for hybrid systems can be a fairly expensive step since it requires evaluation and over-approximation of the continuous dynamics. It has been observed that it is often sufficient to consider fragments of counterexamples rather than complete counterexamples. In this paper we further develop the idea of fragments. We extend the notion of cut sets in directed graphs to cutting sets of fragments in abstractions. Cutting sets of fragments are then used to guide the abstraction refinement in order to prove safety properties for hybrid systems. [ABSTRACT FROM AUTHOR]

Analyses of position and force control laws in the case of perfectly rigid bodies have been made so far with strong assumptions on the state of the contacts such as supposing that they are permanent. We're interested here in having a look at what happens when no such assumptions is made: we are led therefore to propose a Lyapunov stability analysis of a position and force control law in the mathematical framework of nonsmooth Lagrangian dynamical systems, a typical example of hybrid dynamical systems. [ABSTRACT FROM AUTHOR]

In this paper we define a bisimulation concept for some very general models for stochastic hybrid systems (general stochastic hybrid systems). The definition of bisimulation builds on the ideas of Edalat and of Larsen and Skou and of Joyal, Nielsen and Winskel. The main result is that this bisimulation for GSHS is indeed an equivalence relation. The secondary result is that this bisimulation relation for the stochastic hybrid system models used in this paper implies the same kind of bisimulation for their continuous parts and respectively for their jumping structures. Keywords: stochastic hybrid systems, Markov processes, simulation morphism, zigzag morphism, bisimulation, category theory. [ABSTRACT FROM AUTHOR]

This paper focuses on hybrid systems whose discrete state transitions depend on both deterministic and stochastic events. For such systems, after introducing a suitable hybrid model called Discrete Hybrid Stochastic Automaton (DHSA), different finite-time optimal control approaches are examined: (1) Stochastic Hybrid Optimal Control (SHOC), that "optimistically" determines the trajectory providing the best trade off between the tracking performance and the probability that stochastic events realize as expected, under specified chance constraints; (2) Robust Hybrid Optimal Control (RHOC) that, in addition, less optimistically, ensures that the system remains within a specified safety region for all possible realizations of stochastic events. Sufficient conditions for the asymptotic convergence of the state vector are given for receding-horizon implementations of the above schemes. The proposed approaches are exemplified on a simple benchmark problem in production system management. [ABSTRACT FROM AUTHOR]

In this paper, a cascade discrete-continuous state estimator on a partial order is proposed and its existence investigated. The continuous state estimation error is bounded by a monotonically nonincreasing function of the discrete state estimation error, with both the estimation errors converging to zero. This work shows that the lattice approach to estimation is general as the proposed estimator can be constructed for any observable and discrete state observable system. The main advantage of using the lattice approach for estimation becomes clear when the system has monotone properties that can be exploited in the estimator design. In such a case, the computational complexity of the estimator can be drastically reduced and tractability can be achieved. Some examples are proposed to illustrate these ideas. [ABSTRACT FROM AUTHOR]

This paper considers the control of switching power converters which are a particular class of hybrid systems. Such systems, which are controlled by switches, can be modeled using physical principles. Taking advantage of the energetical properties of their models, a Lyapunov function is proposed. This function, which has not to be computed but is systematically deduced from the physical model, allows to derive different stabilizing switching sequences. From a theoretical point of view, asymptotic stability can be obtained, but it requires null intervals between switching times. In order to ensure a minimum time between switchings, this Lyapunov function has to be increasing for a small duration by using a delay or a dead zone. A control law principle that guarantees the invariance of a specified domain with respect to state trajectories is proposed. Two examples are provided at the end of this paper that demonstrate the efficiency of the proposed approach. [ABSTRACT FROM AUTHOR]

The switch-like character of the dynamics of genetic regulatory networks has attracted much attention from mathematical biologists and researchers on hybrid systems alike. We extend our previous work on a method for the qualitative analysis of hybrid models of genetic regulatory networks, based on a class of piecewise-affine differential equation (PADE) models, in two directions. First, we present a refinement of the method using a discrete or qualitative abstraction that preserves stronger properties of the dynamics of the PA systems, in particular the sign patterns of the derivatives of the concentration variables. The discrete transition system resulting from the abstraction is a conservative approximation of the dynamics of the PA system and can be computed symbolically. Second, we apply the refined method to a regulatory system whose functioning is not yet well-understood by biologists, the nutritional stress response in the bacterium Escherichia coli. [ABSTRACT FROM AUTHOR]

The problem of synthesizing feedback controllers that perform sensing and actuation actions on non-uniform and uncertain discrete time domains is considered. This class of problems is relevant to many application domains. For instance, in engine control a heterogenous and, to some extent, uncertain event-driven time domain is due to the behavior of the 4-stroke internal combustion engine, with which the controller has to synchronize to operate the engine properly. Similar problems arise also in standard discrete-time control systems when considering the behavior of the system with controller implementation and communication effects. The design problem is formalized in a hybrid system framework; synthesis and verification methods, based on robust stability and robust performance results, are presented. The effectiveness of the proposed methods is demonstrated in an engine control application. [ABSTRACT FROM AUTHOR]

We study continuous-time switched linear systems with unobserved and exogenous mode signals. We analyze the observability of the initial state and initial mode under arbitrary switching, and characterize both properties in both the autonomous and non-autonomous cases. [ABSTRACT FROM AUTHOR]

By transferring the theory of hybrid systems to a categorical framework, it is possible to develop a homology theory for hybrid systems: hybrid homology. This is achieved by considering the underlying "space" of a hybrid system—its hybrid space or H-space. The homotopy colimit can be applied to this H-space to obtain a single topological space; the hybrid homology of an H-space is the homology of this space. The result is a spectral sequence converging to the hybrid homology of an H-space, providing a concrete way to compute this homology. Moreover, the hybrid homology of the H-space underlying a hybrid system gives useful information about the behavior of this system: the vanishing of the first hybrid homology of this H-space—when it is contractible and finite—implies that this hybrid system is not Zeno. [ABSTRACT FROM AUTHOR]

We consider timed automata whose clocks are imperfect. For a given perturbation error , the perturbed language of a timed automaton is obtained by letting its clocks change at a rate within the interval . We show that the perturbed language of a timed automaton with a single clock can be captured by a deterministic timed automaton. This leads to a decision procedure for the language inclusion problem for systems modeled as products of 1-clock automata with imperfect clocks. We also prove that determinization and decidability of language inclusion are not possible for multi-clock automata, even with perturbation. [ABSTRACT FROM AUTHOR]

We study the class of lazy linear hybrid automata with finite precision. The key features of this class are: The observation of the continuous state and the rate changes associated with mode switchings take place with bounded delays. The values of the continuous variables can be observed with only finite precision. The guards controlling the transitions of the automaton are finite conjunctions of arbitrary linear constraints. We show that the discrete time dynamics of this class of automata can be effectively analyzed without requiring resetting of the continuous variables during mode changes. In fact, our result holds for guard languages that go well beyond linear constraints. [ABSTRACT FROM AUTHOR]

This paper discusses an interpretation of hybrid systems as executable models. A specification of a hybrid system for this purpose can be viewed as a program in a domain-specific programming language. We describe the semantics of HyVisual, which is such a domain-specific programming language. The semantic properties of such a language affect our ability to understand, execute, and analyze a model. We discuss several semantic issues that come in defining such a programming language, such as the interpretation of discontinuities in continuous-time signals, and the interpretation of discrete-event signals in hybrid systems, and the consequences of numerical ODE solver techniques. We describe the solution in HyVisual by giving its operational semantics. [ABSTRACT FROM AUTHOR]

The remarkable drop in the cost of embedded computing, sensing, and actuation is creating an explosion in applications for embedded software. As manufacturers make use of these technologies, they attempt to reduce complexity and contain cost by modularizing their systems and building reconfigurable products from simpler but smarter components. Of particular interest have recently been highly reconfigurable systems, i.e., systems that can be customized, repaired, and upgraded at a fine level of granularity throughout their lifetime. High reconfigurability is putting new demands on the software that is dynamically calibrating, controlling, and coordinating the operations of the system's modules. There is much promise in existing software approaches, in particular in model-based approaches; however, current techniques face a number of new challenges before they can be embedded in the kind of real-time, distributed, and dynamic environment found in highly reconfigurable systems. Here, we discuss challenges, solutions, and lessons learned in the context of a long-term project at PARC to bring such techniques to a highly reconfigurable paper path system. [ABSTRACT FROM AUTHOR]

Semialgebraic computations, i.e., the manipulation of sets and logical conditions defined by polynomial inequalities in real variables, are an essential "primitive" in the analysis and design of hybrid dynamical systems. Fundamental tasks such as reachability analysis, abstraction verification, and the computation of stability and performance certificates, all use these operations extensively, and can quickly become the computational bottleneck in the design process. Although there is a well-developed body of both basic theory and algorithms for these tasks, the practical performance of most available methods is still far from being satisfactory on real-world problems. While there are several possible causes for this (besides the NP-hardness of the task), a sensible explanation lies in the purely algebraic nature of the usual methods, as well as the insistence on exact (as opposed to approximate or "relaxed") solutions. For these reasons, there is a strong interest in the development of efficient techniques for (perhaps restricted) classes of semialgebraic problems. In this talk we review the basic elements and present several new results on the SOS approach to semialgebraic computations, that combines symbolic and numerical techniques from real algebra and convex optimization. Its main defining feature is the use and computation of sum of squares (SOS) decompositions for multivariate polynomials via semidefinite programming. These are extended, using the Positivstellensatz, to structured infeasibility certificates for polynomial equations and inequalities. The developed techniques unify and generalize many well-known existing methods. In particular, we will discuss semialgebraic problems with at most two quantifier alternations (i.e., classical polynomial optimization problems as well as the related games and minimax problems). As an example, we will solve in detail a class of zero-sum two-person games with an infinite number of pure strategies, where the payoff function is a polynomial expression of the actions of the players. Although particular emphasis will be given to the hybrid systems viewpoint, the basic ideas and algorithms, as well as these recent extensions, will be illustrated with examples drawn from a broad range of related domains, including dynamical systems and geometric theorem proving. [ABSTRACT FROM AUTHOR]