A Stability-Based Abstraction Framework for Reach-Avoid Control of Stochastic Dynamical Systems with Unknown Noise Distributions
Finite-state abstractions are widely studied for the automated synthesis of correct-by-construction controllers for stochastic dynamical systems. However, existing abstraction methods often lead to prohibitively large finite-state models. To address this issue, we propose a novel abstraction scheme for stochastic linear systems that exploits the system's stability to obtain significantly smaller abstract models. As a unique feature, we first stabilize the open-loop dynamics using a linear feedback gain. We then use a model-based approach to abstract a known part of the stabilized dynamics while using a data-driven method to account for the stochastic uncertainty. We formalize abstractions as Markov decision processes (MDPs) with intervals of transition probabilities. By stabilizing the dynamics, we can further constrain the control input modeled in the abstraction, which leads to smaller abstract models while retaining the correctness of controllers. Moreover, when the stabilizing feedback controller is aligned with the property of interest, then a good trade-off is achieved between the reduction in the abstraction size and the performance loss. The experiments show that our approach can reduce the size of the graph of abstractions by up to 90% with negligible performance loss.
Code (1)
Similar Papers 제목 키워드 기반
Symmetry-based Abstraction Algorithm for Accelerating Symbolic Control Synthesis
We propose an efficient symbolic control synthesis algorithm for equivariant continuous-time dynamical systems to satisfy reach-avoid specifications. The algorithm exploits dynamical symmetries to construct lean abstract…
PositionCorrect-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 …
Continuous ControlAbstraction-Free Control Synthesis to Satisfy Temporal Logic Constraints under Sensor Faults and Attacks
We study the problem of synthesizing a controller to satisfy a complex task in the presence of sensor faults and attacks. We model the task using Gaussian distribution temporal logic (GDTL), and propose a solution approa…
State EstimationData-driven Interval MDP for Robust Control Synthesis
The abstraction of dynamical systems is a powerful tool that enables the design of feedback controllers using a correct-by-design framework. We investigate a novel scheme to obtain data-driven abstractions of discrete-ti…
Reach-Avoid Control Synthesis for a Quadrotor UAV with Formal Safety Guarantees
Reach-avoid specifications are one of the most common tasks in autonomous aerial vehicle (UAV) applications. Despite the intensive research and development associated with control of aerial vehicles, generating feasible …