Old-established methods in a new look: How HyPro speeds up reachability computations for hybrid systems
ABSTRACT. Reachability analysis for hybrid systems is a highly challenging task. Besides logical approaches, methods based on flowpipe construction are in use, implemented in several tools. Despite exciting developments, these tools are still not ready for large-scale applications. In this talk we discuss how well-known techniques like over-approximation, counterexample-guided abstraction refinement or parallelization can be instantiated in this context to reduce the computational effort in practice, and how these ideas are implemented in the HyPro tool.
Compositional Synthesis of Finite Abstractions for Continuous-Space Stochastic Control Systems: A Small-Gain Approach
ABSTRACT. This paper is concerned with a compositional approach for constructing finite abstractions (a.k.a. finite Markov decision processes) of interconnected discrete-time stochastic control systems. The proposed framework is based on a notion of so-called stochastic simulation function enabling us to use an abstract system as a substitution of the original one in the controller design process with guaranteed error bounds. In the first part of the paper, we derive sufficient small-gain type conditions for the compositional quantification of the distance in probability between the interconnection of stochastic control subsystems and that of their (finite or infinite) abstractions. In the second part of the paper, we construct finite abstractions together with their corresponding stochastic simulation functions for the class of linear stochastic control systems. We apply our results to the temperature regulation in a circular building by constructing compositionally a finite abstraction of a network containing 1000 rooms. We use the constructed finite abstractions as substitutes to synthesize policies compositionally regulating the temperature in each room for a bounded time horizon.
Temporal Logic Control of POMDPs Via Label-Based Stochastic Simulation Relations
ABSTRACT. The synthesis of controllers guaranteeing linear temporal logic specifications on partially observable Markov decision processes (POMDP) via their belief models causes computational issues due to the continuous spaces. In this work, we construct a finite-state abstraction on which a control policy is synthesized and refined back to the original belief model. We introduce a new notion of label- based approximate stochastic simulation to quantify the deviation between belief models. We develop a robust synthesis methodology that yields a lower bound on the satisfaction probability, by compensating for deviations a priori, and that utilizes a less conservative control refinement.
Concentration of Measure for Chance-Constrained Optimization
ABSTRACT. Chance-constrained optimization problems optimize a cost function in the presence of probabilistic constraints. They are convex in very special cases and, in practice, they are solved using approximation techniques. In this paper, we study approximation of chance constraints for the class of probability distributions that satisfy a concentration of measure property. We show that using concentration of measure, we can transform chance constraints to constraints on expectations, which can then be solved based on scenario optimization. Our approach depends solely on the concentration of measure property of the uncertainty and does not require the objective or constraint functions to be convex. We also give bounds on the required number of scenarios for achieving a certain confidence. We demonstrate our approach on a non-convex chanced-constrained optimization, and benchmark our technique against alternative approaches in the literature on chance-constrained LQG problem.
ABSTRACT. This paper considers control synthesis for polynomial control systems. The developed method leans upon Lyapunov stability and Bernstein certificates of positivity. We strive to develop an algorithm that computes a polynomial control and a polynomial Lyaponov function in the simplicial Bernstein form. Subsequently, we reduce the control synthesis problem to a finite number of evaluations of a polynomial within Bernstein coefficient bounds representing controls and Lyapunov functions. As a consequence, the equilibrium is asymptotically stable with this control.
Control Synthesis and Classification for Unicycle Dynamics Using the Gradient and Value Sampling Particle Filters
ABSTRACT. Value functions arising from dynamic programming can be used to synthesize optimal control inputs for general nonlinear systems with state and/or input constraints; however, the inputs generated by steepest descent on these value functions often lead to chattering behavior. In [Traft & Mitchell, 2016] we proposed the Gradient Sampling Particle Filter (GSPF), which combines robot state estimation and nonsmooth optimization algorithms to alleviate this problem. In this paper we extend the GSPF to velocity controlled unicycle (or equivalently differential drive) dynamics. We also show how the algorithm can be adapted to classify whether an exogenous input—such as one arising from shared human-in-the-loop control—is desirable. The two algorithms are demonstrated on a ground robot.
An Interval-Based Sliding Horizon Motion Planning Method
ABSTRACT. A new algorithm of motion planning based on set-membership approach is presented. The goal of this algorithm is to find a safe and optimal path taking into account various sources of bounded uncertainties on the dynamical model of the plant, on the model of the environment, while being robust with respect to the numerical approximations introduced by numerical integration methods. The main approach is based on a sliding horizon method to predict the behavior of the system allowing the computation of an optimal path. As an example, the motion planning algorithm is applied to an Autonomous Underwater Vehicle (AUV) case study, showing the benefit of the proposed approach.
Workshops dinner at Keble College. Drinks reception from 7pm, to be seated by 7:30 (pre-booking via FLoC registration system required; guests welcome).