-
Provably Correct Sensor-driven Path-following for Unicycles using Monotonic Score Functions
Authors:
Benton Clark,
Varun Hariprasad,
Hasan A. Poonawala
Abstract:
This paper develops a provably stable sensor-driven controller for path-following applications of robots with unicycle kinematics, one specific class of which is the wheeled mobile robot (WMR). The sensor measurement is converted to a scalar value (the score) through some map** (the score function); the latter may be designed or learned. The score is then mapped to forward and angular velocities…
▽ More
This paper develops a provably stable sensor-driven controller for path-following applications of robots with unicycle kinematics, one specific class of which is the wheeled mobile robot (WMR). The sensor measurement is converted to a scalar value (the score) through some map** (the score function); the latter may be designed or learned. The score is then mapped to forward and angular velocities using a simple rule with three parameters. The key contribution is that the correctness of this controller only relies on the score function satisfying monotonicity conditions with respect to the underlying state -- local path coordinates -- instead of achieving specific values at all states. The monotonicity conditions may be checked online by moving the WMR, without state estimation, or offline using a generative model of measurements such as in a simulator. Our approach provides both the practicality of a purely measurement-based control and the correctness of state-based guarantees. We demonstrate the effectiveness of this path-following approach on both a simulated and a physical WMR that use a learned score function derived from a binary classifier trained on real depth images.
△ Less
Submitted 21 March, 2023;
originally announced March 2023.
-
Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions
Authors:
Thom Badings,
Licio Romao,
Alessandro Abate,
David Parker,
Hasan A. Poonawala,
Marielle Stoelinga,
Nils Jansen
Abstract:
Controllers for dynamical systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modeled as process noise in a dynamical system, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distri…
▽ More
Controllers for dynamical systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modeled as process noise in a dynamical system, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. In particular, we address the problem of computing a controller that provides probabilistic guarantees on safely reaching a target, while also avoiding unsafe regions of the state space. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. As a key contribution, we adapt tools from the scenario approach to compute probably approximately correct (PAC) bounds on these transition probabilities, based on a finite number of samples of the noise. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP). This iMDP is, with a user-specified confidence probability, robust against uncertainty in the transition probabilities, and the tightness of the probability intervals can be controlled through the number of samples. We use state-of-the-art verification techniques to provide guarantees on the iMDP and compute a controller for which these guarantees carry over to the original control system. In addition, we develop a tailored computational scheme that reduces the complexity of the synthesis of these guarantees on the iMDP. Benchmarks on realistic control systems show the practical applicability of our method, even when the iMDP has hundreds of millions of transitions.
△ Less
Submitted 4 January, 2023;
originally announced January 2023.
-
Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise
Authors:
Thom S. Badings,
Alessandro Abate,
Nils Jansen,
David Parker,
Hasan A. Poonawala,
Marielle Stoelinga
Abstract:
Controllers for autonomous systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modelled as process noise, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a…
▽ More
Controllers for autonomous systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modelled as process noise, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a novel planning method that does not rely on any explicit representation of the noise distributions. In particular, we address the problem of computing a controller that provides probabilistic guarantees on safely reaching a target. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. As a key contribution, we adapt tools from the scenario approach to compute probably approximately correct (PAC) bounds on these transition probabilities, based on a finite number of samples of the noise. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP). This iMDP is robust against uncertainty in the transition probabilities, and the tightness of the probability intervals can be controlled through the number of samples. We use state-of-the-art verification techniques to provide guarantees on the iMDP, and compute a controller for which these guarantees carry over to the autonomous system. Realistic benchmarks show the practical applicability of our method, even when the iMDP has millions of states or transitions.
△ Less
Submitted 13 December, 2021; v1 submitted 25 October, 2021;
originally announced October 2021.
-
Correct-by-construction reach-avoid control of partially observable linear stochastic systems
Authors:
Thom Badings,
Hasan A. Poonawala,
Marielle Stoelinga,
Nils Jansen
Abstract:
We study feedback controller synthesis for reach-avoid control of discrete-time, linear time-invariant (LTI) systems with Gaussian process and measurement noise. The problem is to compute a controller such that, with at least some required probability, the system reaches a desired goal state in finite time while avoiding unsafe states. Due to stochasticity and nonconvexity, this problem does not a…
▽ More
We study feedback controller synthesis for reach-avoid control of discrete-time, linear time-invariant (LTI) systems with Gaussian process and measurement noise. The problem is to compute a controller such that, with at least some required probability, the system reaches a desired goal state in finite time while avoiding unsafe states. Due to stochasticity and nonconvexity, this problem does not admit exact algorithmic or closed-form solutions in general. Our key contribution is a correct-by-construction controller synthesis scheme based on a finite-state abstraction of a Gaussian belief over the unmeasured state, obtained using a Kalman filter. We formalize this abstraction as a Markov decision process (MDP). To be robust against numerical imprecision in approximating transition probabilities, we use MDPs with intervals of transition probabilities. By construction, any policy on the abstraction can be refined into a piecewise linear feedback controller for the LTI system. We prove that the closed-loop LTI system under this controller satisfies the reach-avoid problem with at least the required probability. The numerical experiments show that our method is able to solve reach-avoid problems for systems with up to 6D state spaces, and with control input constraints that cannot be handled by methods such as the rapidly-exploring random belief trees (RRBT).
△ Less
Submitted 12 September, 2023; v1 submitted 3 March, 2021;
originally announced March 2021.
-
A Deep Ensemble Multi-Agent Reinforcement Learning Approach for Air Traffic Control
Authors:
Supriyo Ghosh,
Sean Laguna,
Shiau Hong Lim,
Laura Wynter,
Hasan Poonawala
Abstract:
Air traffic control is an example of a highly challenging operational problem that is readily amenable to human expertise augmentation via decision support technologies. In this paper, we propose a new intelligent decision making framework that leverages multi-agent reinforcement learning (MARL) to dynamically suggest adjustments of aircraft speeds in real-time. The goal of the system is to enhanc…
▽ More
Air traffic control is an example of a highly challenging operational problem that is readily amenable to human expertise augmentation via decision support technologies. In this paper, we propose a new intelligent decision making framework that leverages multi-agent reinforcement learning (MARL) to dynamically suggest adjustments of aircraft speeds in real-time. The goal of the system is to enhance the ability of an air traffic controller to provide effective guidance to aircraft to avoid air traffic congestion, near-miss situations, and to improve arrival timeliness. We develop a novel deep ensemble MARL method that can concisely capture the complexity of the air traffic control problem by learning to efficiently arbitrate between the decisions of a local kernel-based RL model and a wider-reaching deep MARL model. The proposed method is trained and evaluated on an open-source air traffic management simulator developed by Eurocontrol. Extensive empirical results on a real-world dataset including thousands of aircraft demonstrate the feasibility of using multi-agent RL for the problem of en-route air traffic control and show that our proposed deep ensemble MARL method significantly outperforms three state-of-the-art benchmark approaches.
△ Less
Submitted 3 April, 2020;
originally announced April 2020.
-
FASTER: Fusion AnalyticS for public Transport Event Response
Authors:
Sebastien Blandin,
Laura Wynter,
Hasan Poonawala,
Sean Laguna,
Basile Dura
Abstract:
Increasing urban concentration raises operational challenges that can benefit from integrated monitoring and decision support. Such complex systems need to leverage the full stack of analytical methods, from state estimation using multi-sensor fusion for situational awareness, to prediction and computation of optimal responses. The FASTER platform that we describe in this work, deployed at nation…
▽ More
Increasing urban concentration raises operational challenges that can benefit from integrated monitoring and decision support. Such complex systems need to leverage the full stack of analytical methods, from state estimation using multi-sensor fusion for situational awareness, to prediction and computation of optimal responses. The FASTER platform that we describe in this work, deployed at nation scale and handling 1.5 billion public transport trips a year, offers such a full stack of techniques for this large-scale, real-time problem. FASTER provides fine-grained situational awareness and real-time decision support with the objective of improving the public transport commuter experience. The methods employed range from statistical machine learning to agent-based simulation and mixed-integer optimization. In this work we present an overview of the challenges and methods involved, with details of the commuter movement prediction module, as well as a discussion of open problems.
△ Less
Submitted 14 May, 2019;
originally announced June 2019.
-
Robust commuter movement inference from connected mobile devices
Authors:
Baoyang Song,
Hasan Poonawala,
Laura Wynter,
Sebastien Blandin
Abstract:
The preponderance of connected devices provides unprecedented opportunities for fine-grained monitoring of the public infrastructure. However while classical models expect high quality application-specific data streams, the promise of the Internet of Things (IoT) is that of an abundance of disparate and noisy datasets from connected devices. In this context, we consider the problem of estimation o…
▽ More
The preponderance of connected devices provides unprecedented opportunities for fine-grained monitoring of the public infrastructure. However while classical models expect high quality application-specific data streams, the promise of the Internet of Things (IoT) is that of an abundance of disparate and noisy datasets from connected devices. In this context, we consider the problem of estimation of the level of service of a city-wide public transport network. We first propose a robust unsupervised model for train movement inference from wifi traces, via the application of robust clustering methods to a one dimensional spatio-temporal setting. We then explore the extent to which the demand-supply gap can be estimated from connected devices. We propose a classification model of real-time commuter patterns, including both a batch training phase and an online learning component. We describe our deployment architecture and assess our system accuracy on a large-scale anonymized dataset comprising more than 10 billion records.
△ Less
Submitted 3 March, 2019;
originally announced March 2019.
-
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Authors:
Murat Cubuktepe,
Nils Jansen,
Sebastian Junges,
Joost-Pieter Katoen,
Ivan Papusha,
Hasan A. Poonawala,
Ufuk Topcu
Abstract:
Multi-objective verification problems of parametric Markov decision processes under optimality criteria can be naturally expressed as nonlinear programs. We observe that many of these computationally demanding problems belong to the subclass of signomial programs. This insight allows for a sequential optimization algorithm to efficiently compute sound but possibly suboptimal solutions. Each stage…
▽ More
Multi-objective verification problems of parametric Markov decision processes under optimality criteria can be naturally expressed as nonlinear programs. We observe that many of these computationally demanding problems belong to the subclass of signomial programs. This insight allows for a sequential optimization algorithm to efficiently compute sound but possibly suboptimal solutions. Each stage of this algorithm solves a geometric programming problem. These geometric programs are obtained by convexifying the nonconvex constraints of the original problem. Direct applications of the encodings as nonlinear pro- grams are model repair and parameter synthesis. We demonstrate the scalability and quality of our approach by well-known benchmarks
△ Less
Submitted 25 January, 2017;
originally announced February 2017.
