arXiv subjects

Hasan A. Poonawala

Publications and source records attributed to Hasan A. Poonawala.

10 recordsLinked to original sources

arXiv2026

Geometric Conditions for Lossless Convexification in Linear Optimal Control with Discrete-Valued Inputs: Real-Time Implementation for Spacecraft Rendezvous

Optimal control problems with discrete-valued inputs are inherently challenging due to their mixed-integer nature, rendering them generally intractable for real-time, safety-critical aerospace applications. Lossless convexification offers a powerful alternative by reformulating these mixed-integer programs into computationally efficient convex programs. This paper develops a lossless convexification framework for the optimal control of linear time-varying systems with discrete-valued inputs. We extend existing theoretical results by demonstrating that system normality is preserved when reformulating Lagrange-form problems into Mayer-form via an epigraph transformation. Furthermore, we establish that under simple geometric conditions on the input set, the solution to the relaxed convex problem strictly satisfies the original non-convex input constraints. This framework enables the real-time computation of optimal discrete-valued controls without resorting to mixed-integer optimization. The proposed algorithm is validated on a spacecraft rendezvous maneuver utilizing discrete-valued reaction thrusters in an elliptical orbit. Numerical results from Monte Carlo simulations confirm that the algorithm consistently yields exact discrete-valued control inputs with computational timelines compatible with safety-critical, on-board applications.

math.OC↗

arXiv2026

ReLU Barrier Functions for Nonlinear Systems with Constrained Control: A Union of Invariant Sets Approach

Certifying safety for nonlinear systems with polytopic input constraints is challenging because CBF synthesis must ensure control admissibility under saturation. We propose an approximation--verification pipeline that performs convex barrier synthesis on piecewise-affine (PWA) surrogates and certifies safety for the original nonlinear system via facet-wise verification. To reduce conservatism while preserving tractability, we use a two-slope Leaky ReLU surrogate for the extended class-$\mathcal{K}$ function $α(\cdot)$ and combine multiple certificates using a Union of Invariant Sets (UIS). Counterexamples are handled through local uncertainty updates. Simulations on pendulum and cart-pole systems with input saturation show larger certified invariant sets than linear-$α$ designs with tractable computation time.

eess.SY↗

arXiv2024

Invariant Set Estimation for Piecewise Affine Dynamical Systems Using Piecewise Affine Barrier Function

This paper introduces an algorithm for approximating the invariant set of closed-loop controlled dynamical systems identified using ReLU neural networks or piecewise affine PWA functions, particularly addressing the challenge of providing safety guarantees for ReLU networks commonly used in safety-critical applications. The invariant set of PWA dynamical system is estimated using ReLU networks or its equivalent PWA function. This method entails formulating the barrier function as a PWA function and converting the search process into a linear optimization problem using vertices. We incorporate a domain refinement strategy to increase flexibility in case the optimization does not find a valid barrier function. Moreover, the objective of optimization is to maximize the invariant set based on the current partition. Our experimental results demonstrate the effectiveness and efficiency of our approach, demonstrating its potential for ensuring the safety of PWA dynamical systems.

eess.SY↗

arXiv2023

Automated Stability Analysis of Piecewise Affine Dynamics Using Vertices

This paper presents an automated algorithm to analyze the stability of piecewise affine (PWA) dynamical systems due to their broad applications. We parametrize the Lyapunov function as a PWA function, with polytopic regions defined by the PWA dynamics. Using this parametrization, Stability conditions can be expressed as linear constraints restricted to polytopes so that the search for a Lyapunov function involves solving a linear program. However, a valid Lyapunov function might not be found given these polytopic regions. A natural response is to increase the size of the parametrization of the Lyapunov function by dividing regions and solving the new linear program. This paper proposes two new methods to divide each polytope into smaller ones. The first approach divides a polytope based on the sign of the derivative of the candidate Lyapunov function, while the second divides it based on the change in the vector field of the PWA dynamical system. In addition, we propose using Delaunay triangulation to achieve automated division of regions and preserve the continuity of the PWA Lyapunov function. Examples involving learned models and explicit MPC controllers demonstrate that the proposed method of dividing regions leads to valid Lyapunov functions with fewer regions than existing methods, reducing the computational time taken for stability analysis

eess.SY↗

arXiv2023

Correct-by-construction reach-avoid control of partially observable linear stochastic systems

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).

cs.AI↗

arXiv2023

Provably Correct Sensor-driven Path-following for Unicycles using Monotonic Score Functions

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 mapping (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.

eess.SY↗

arXiv2023

Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions

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.

eess.SY↗

arXiv2021

Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise

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.

eess.SY↗

arXiv2019

Training Classifiers For Feedback Control

One approach for feedback control using high dimensional and rich sensor measurements is to classify the measurement into one out of a finite set of situations, each situation corresponding to a (known) control action. This approach computes a control action without estimating the state. Such classifiers are typically learned from a finite amount of data using supervised machine learning algorithms. We model the closed-loop system resulting from control with feedback from classifier outputs as a piece-wise affine differential inclusion. We show how to train a linear classifier based on performance measures related to learning from data and the local stability properties of the resulting closed-loop system. The training method is based on the projected gradient descent algorithm. We demonstrate the advantage of training classifiers using control-theoretic properties on a case study involving navigation using range-based sensors.

math.OC↗

arXiv2017

Sequential Convex Programming for the Efficient Verification of Parametric MDPs

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

cs.LO↗