Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Backstepping Reach-avoid Controller Synthesis for Multi-input Multi-output Systems with Mixed Relative Degrees

Jianqiang Ding, Dingran Yuan, Shankar A. Deka

TL;DR

The paper addresses the need for provable reach-avoid guarantees in safety-critical CPS, particularly for high-dimensional MIMO systems with mixed relative degrees. It unifies safety and reachability by constructing Exponential Control Guidance-barrier Functions (ECGBFs) and leveraging SOS optimization, feedback linearization, and backstepping to synthesize controllers that keep outputs within a safe set $\mathcal{C}$ and drive them to a target set $\mathcal{X}^r$. A key contribution is a two-stage design: first solve a reach-avoid problem for a single-integrator via SOS, then extend to the full MIMO system through backstepping, yielding a constructive ECGBF $\Psi(\mathbf{x})$ and a recursive controller $\mathbf{k}(\mathbf{x})$ with formal guarantees. Demonstrations on examples like a Dubins car and a planar robotic arm show trajectories remain in $\mathcal{C}$ and converge to $\mathcal{X}^r$, with $\Psi(\mathbf{x})$ monotonically increasing along trajectories, highlighting the method's scalability and practical impact for safety-critical, high-dimensional systems.

Abstract

Designing controllers with provable formal guarantees has become an urgent requirement for cyber-physical systems in safety-critical scenarios. Beyond addressing scalability in high-dimensional implementations, controller synthesis methodologies separating safety and reachability objectives may risk optimization infeasibility due to conflicting constraints, thereby significantly undermining their applicability in practical applications. In this paper, by leveraging feedback linearization and backstepping techniques, we present a novel framework for constructing provable reach-avoid formal certificates tailored to multi-input multi-output systems. Based on this, we developed a systematic synthesis approach for controllers with reach-avoid guarantees, which ensures that the outputs of the system eventually enter the predefined target set while staying within the required safe set. Finally, we demonstrate the effectiveness of our method through simulations.

Backstepping Reach-avoid Controller Synthesis for Multi-input Multi-output Systems with Mixed Relative Degrees

TL;DR

The paper addresses the need for provable reach-avoid guarantees in safety-critical CPS, particularly for high-dimensional MIMO systems with mixed relative degrees. It unifies safety and reachability by constructing Exponential Control Guidance-barrier Functions (ECGBFs) and leveraging SOS optimization, feedback linearization, and backstepping to synthesize controllers that keep outputs within a safe set and drive them to a target set . A key contribution is a two-stage design: first solve a reach-avoid problem for a single-integrator via SOS, then extend to the full MIMO system through backstepping, yielding a constructive ECGBF and a recursive controller with formal guarantees. Demonstrations on examples like a Dubins car and a planar robotic arm show trajectories remain in and converge to , with monotonically increasing along trajectories, highlighting the method's scalability and practical impact for safety-critical, high-dimensional systems.

Abstract

Designing controllers with provable formal guarantees has become an urgent requirement for cyber-physical systems in safety-critical scenarios. Beyond addressing scalability in high-dimensional implementations, controller synthesis methodologies separating safety and reachability objectives may risk optimization infeasibility due to conflicting constraints, thereby significantly undermining their applicability in practical applications. In this paper, by leveraging feedback linearization and backstepping techniques, we present a novel framework for constructing provable reach-avoid formal certificates tailored to multi-input multi-output systems. Based on this, we developed a systematic synthesis approach for controllers with reach-avoid guarantees, which ensures that the outputs of the system eventually enter the predefined target set while staying within the required safe set. Finally, we demonstrate the effectiveness of our method through simulations.
Paper Structure (7 sections, 3 theorems, 35 equations, 5 figures, 1 table, 1 algorithm)

This paper contains 7 sections, 3 theorems, 35 equations, 5 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries and Background
  3. Reach-avoid Controller Synthesis
  4. Feedback Linearization
  5. Reach-avoid backstepping
  6. Experiments
  7. Conclusion

Key Result

Theorem 1

xue2024reach Given the safe output set $\mathcal{C}$ and target output set $\mathcal{X}^{r}$ satisfying assumption assumption on sets, if the function $\psi(\bm{y}(\cdot)): \mathbb{R}^{n}\rightarrow \mathbb{R}$ is an ECGBF, then any Lipschitz continuous controller $\bm{u}(\bm{x}) \in \mathcal{K}_{e} with

Figures (5)

  • Figure 1: $100$ randomly sampled trajectories (dashed line from orange to green cross) of system \ref{['eq: ex1 system']} with synthesized reach-avoid controller. The grey vector-field indicates the function $\bm{k}_1(\bm{y}(\bm{x}))$, from which we construct $\bm{k}(\bm{y}(\bm{x}))$ via backstepping.
  • Figure 2: Evaluation of $\Psi(\bm{x})$ along $100$ randomly sampled trajectories.
  • Figure 3: Simulated trajectories (dashed line from orange dot to green cross) of Dubins car on a racetrack with synthesized reach-avoid controller. The grey vector field indicates the function $\bm{k}_1(\bm{y}(\bm{x}))$, from which we construct $\bm{k}(\bm{y}(\bm{x}))$ via backstepping.
  • Figure 4: Simulated trajectories (dashed line from orange dot to green cross) of 2-link planar robotic arm. The grey vector field indicates the function $\bm{k}_1(\bm{y}(\bm{x}))$, from which we construct $\bm{k}(\bm{y}(\bm{x}))$ via backstepping.
  • Figure 5: Impact of increasing $\mu_l^i$ on $\mathcal{C}_\Psi$. Color bar indicates the different values of $\mu_l^i$.

Theorems & Definitions (12)

  • Definition 1
  • Theorem 1
  • Definition 2
  • Remark 1
  • Theorem 2
  • proof
  • Proposition 1
  • proof
  • Remark 2
  • Example 1
  • ...and 2 more