ABSTRACT. We define robust abstractions for synthesizing provably correct and robust controllers for (possibly infinite) transition systems with inputs subject to uncertainty modelled by additional transitions. It is shown that robust abstractions are sound in the sense that they preserve robust satisfaction of linear-time properties. We then focus on discrete-time control systems modelled by nonlinear difference equations with inputs and define concrete robust abstractions for them. While most abstraction techniques in the literature for nonlinear systems focus on constructing sound abstractions, we present computational procedures for constructing both sound and approximately complete robust abstractions for general nonlinear control systems without stability assumptions. Such procedures are complete in the sense that, given a concrete discrete-time control system and an arbitrarily small perturbation of this system, there exists a finite transition system that robustly abstracts the concrete system and is abstracted by the slightly perturbed system simultaneously. Consequently, the existence of controllers for a general discrete-time nonlinear control system and linear-time specifications is robustly decidable: if a specification is robustly realizable, there is a decision procedure to find a (potentially less) robust control strategy. The theoretical results are illustrated with a simple motion planning example.

ABSTRACT. In this paper, we describe an abstraction based method for synthesizing a state based switching control for stabilizing a family of dynamical systems. Given a set of dynamical systems and a set of polyhedral switching surfaces, the algorithm synthesizes a strategy that assigns to every surface the linear dynamics to switch to at the surface. Our algorithm constructs a finite game graph that consists of the switching surfaces as the existential nodes and the choices of the dynamics as the universal nodes. In addition, the edges capture quantitative information about the evolution of the distance of the state from the equilibrium point along the executions. A switching strategy for the family of dynamical systems is extracted by finding a strategy on the game graph which result in plays having a bounded weight. Such a strategy is obtained by reducing the problem to the strategy synthesis for an energy game, which is a well-studied problem in the literature. We have implemented our algorithm for polyhedral inclusion dynamics and linear dynamics. We illustrate our algorithm on examples from these two classes of systems.

ABSTRACT. A new control method for nonlinear systems is presented which solves reach-avoid problems by interpolating optimal solutions using convex combinations. It also provides formal guarantees for constraint satisfaction and safety. Reach-avoid problems are important control tasks, which arise in many modern cyber-physical systems, including autonomous driving and robotic path planning. By computing the optimal input trajectories for finitely many extreme states only and combining them using convex combinations for all states in a continuous set, we obtain an efficient control policy. Moreover, our approach has very low online computation complexity, making it applicable for fast dynamical systems. Iterating through our approach leads to a new form of feedback control with formal guarantees in the presence of disturbances. We demonstrate the new control method for a control problem in automated driving and show the advantages compared to a classical control method.

ABSTRACT. Timing contracts for embedded controller implementation specify the constraints on the time instants at which certain operations are performed such as sampling, actuation, computation, etc. Several previous works have focused on stability analysis of embedded control systems under such timing contracts. In this paper, we consider the scheduling of embedded controllers on a shared computational platform. Given a set of controllers, each of which is subject to a timing contract, we synthesize a dynamic scheduling policy, which guarantees that each timing contract is satisfied and that the shared computational resource is allocated to at most one embedded controller at any time. The approach is based on a timed game formulation whose solution provides a suitable scheduling policy. In the second part of the paper, we consider the problem of synthesizing a set of timing contracts that guarantee at the same time the schedulability and the stability of the embedded controllers.

ABSTRACT. Humanoid robots walking across intermittent terrain, robotic arms grasping multifaceted objects, UAVs darting left or right around a tree, or autonomous vehicles making discrete navigation decisions in traffic… many of the dynamics and control problems we face today have both rich nonlinear dynamics and an inherently combinatorial structure. In this talk, I’ll review some recent work on optimization-based planning and control methods which address these two challenges simultaneously.  All of these can be modeled as hybrid systems, but in some cases more efficient optimizations are possible by using alternative formulations, such as (measure-) differential inclusions.  I’ll present our explorations with mixed-integer convex-, semidefinite-programming-relaxations, and satisfiability-modulo-theory(SMT)-based methods applied to hard problems in legged locomotion over rough terrain, grasp optimization, and UAVs flying through highly cluttered environments.

ABSTRACT. We have recently constructed a piecewise quadratic Lyapunov function to prove the boundedness of the reachable values set of piecewise affine discrete-time systems. The method developed also provided an overapproximation of the reachable values set. In this paper, we refine the latter overapproximation extending previous works combining policy iterations with quadratic Lyapunov functions.

ABSTRACT. Timed automata have an idealized semantics where clocks are assumed to be perfectly continuous and synchronized, and guards have infinite precision. These assumptions cannot be realized physically. In order to ensure that correct timed automata designs can be implemented on real-time platforms, several authors have suggested that timed automata be studied under robust semantics. A timed automaton H is said to robustly satisfy a property if there is a positive ε and/or a positive δ such that the automaton satisfies the property even when the clocks are allowed to drift by ε and/or guards are enlarged by δ. In this paper we show that, 1. checking ω-regular properties when only clocks are perturbed or when both clocks and guards are perturbed are PSPACE-complete; and 2. one can compute the exact reachable set of a bounded timed automaton when clocks are drifted by infinitesimally small amount, using polynomial space. In particular, we remove the restrictive assumption on the timed automaton that its region graph does not contain certain progress cycles, under which the above results have been proved previously.

ABSTRACT. In this paper, we propose an approach to automatically compute invariant clusters for nonlinear semialgebraic hybrid systems. An invariant cluster for an ordinary differential equation (ODE) is a multivariate polynomial invariant g(u,x)=0, parametric in u, which can yield an infinite number of concrete invariants by assigning different values to u so that every trajectory of the system can be overapproximated precisely by the intersection of a group of concrete invariants. For semialgebraic systems, which involve ODEs with multivariate polynomial vector flow, given a template multivariate polynomial g(u,x), an invariant clusters can be obtained by first computing the remainder of the Lie derivative of g(u,x) divided by g(u,x) and then solving the system of polynomial equations obtained from the coefficients of the remainder. Based on invariant clusters and sum-of-squares (SOS) programming, we present a new method for the safety verification of hybrid systems. Experiments on nonlinear benchmark systems from biology and control theory show that our approach is effective and efficient.

ABSTRACT. Simulations are a practical method of increasing the confidence that a system design is correct. This paper presents techniques which aim to determine all the states that can be reached using a particular hybrid automaton simulation algorithm, a property we call simulation-equivalent reachability. Although this is a slightly weaker property than traditional reachability, its computation can be efficient and accurate.

We present HyLAA, the first tool for simulation-equivalent reachability of linear hybrid automata. HyLAA's analysis is exact; upon completion, the tool provides a concrete simulation trace to an unsafe state if and only if the hybrid automaton simulation engine could produce such a trace. In the backend, the tool implements an efficient algorithm for continuous post that exploits the superposition principle of linear systems, requiring only n+1 simulations per mode for an n-dimensional linear system. This technique is capable of analyzing a replicated helicopter system with over 1000 state variables in less than 20 minutes. The tool also contains several novel enhancements to improve its efficiency, including invariant constraint elimination, warm-start linear programming, and trace-guided set deaggregation.