Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Context-triggered Abstraction-based Control Design

Satya Prakash Nayak, Lucas Neves Egidio, Matteo Della Rossa, Anne-Kathrin Schmuck, Raphaël Jungers

TL;DR

This work tackles automatic synthesis of provably correct hybrid controllers for nonlinear dynamical systems under arbitrary LTL specifications, including context switches triggered by the environment. It introduces a two-layer architecture where the high-level logical layer and a low-level control layer exchange information via strategy templates and context-dependent reach-while-avoid objectives, all without relying on brute-force grid discretization. A novel augmented parity-game framework and a dedicated solver enable end-to-end synthesis, while a CLF-based low-level design provides certified control policies that realize the high-level strategy. The approach demonstrates scalability and applicability to complex CPS scenarios, offering a principled, discretization-free path to reactive, correct-by-construction control.

Abstract

We consider the problem of automatically synthesizing a hybrid controller for non-linear dynamical systems which ensures that the closed-loop fulfills an arbitrary \emph{Linear Temporal Logic} specification. Moreover, the specification may take into account logical context switches induced by an external environment or the system itself. Finally, we want to avoid classical brute-force time- and space-discretization for scalability. We achieve these goals by a novel two-layer strategy synthesis approach, where the controller generated in the lower layer provides invariant sets and basins of attraction, which are exploited at the upper logical layer in an abstract way. In order to achieve this, we provide new techniques for both the upper- and lower-level synthesis. Our new methodology allows to leverage both the computing power of state space control techniques and the intelligence of finite game solving for complex specifications, in a scalable way.

Context-triggered Abstraction-based Control Design

TL;DR

This work tackles automatic synthesis of provably correct hybrid controllers for nonlinear dynamical systems under arbitrary LTL specifications, including context switches triggered by the environment. It introduces a two-layer architecture where the high-level logical layer and a low-level control layer exchange information via strategy templates and context-dependent reach-while-avoid objectives, all without relying on brute-force grid discretization. A novel augmented parity-game framework and a dedicated solver enable end-to-end synthesis, while a CLF-based low-level design provides certified control policies that realize the high-level strategy. The approach demonstrates scalability and applicability to complex CPS scenarios, offering a principled, discretization-free path to reactive, correct-by-construction control.

Abstract

We consider the problem of automatically synthesizing a hybrid controller for non-linear dynamical systems which ensures that the closed-loop fulfills an arbitrary \emph{Linear Temporal Logic} specification. Moreover, the specification may take into account logical context switches induced by an external environment or the system itself. Finally, we want to avoid classical brute-force time- and space-discretization for scalability. We achieve these goals by a novel two-layer strategy synthesis approach, where the controller generated in the lower layer provides invariant sets and basins of attraction, which are exploited at the upper logical layer in an abstract way. In order to achieve this, we provide new techniques for both the upper- and lower-level synthesis. Our new methodology allows to leverage both the computing power of state space control techniques and the intelligence of finite game solving for complex specifications, in a scalable way.
Paper Structure (30 sections, 17 theorems, 32 equations, 8 figures, 1 algorithm)

This paper contains 30 sections, 17 theorems, 32 equations, 8 figures, 1 algorithm.

Table of Contents

  1. INTRODUCTION
  2. Motivating Example, Challenges and Contributions
  3. Literature Review
  4. PRELIMINARIES
  5. Dynamical Systems
  6. Linear Temporal Logic
  7. Games on Graphs
  8. Strategy Templates
  9. PROBLEM STATEMENT
  10. SYNTHESIS OVERVIEW
  11. High-Level Logical Synthesis
  12. The Top-Down Interface
  13. Reach-While-Avoid-Objectives
  14. Feedback-Control Policies
  15. The Bottom-Up Interface
  16. ...and 15 more sections

Key Result

Lemma 1

Consider a control system $\mathcal{S}:=(X,U,f)$, a compact target set $X_T\subset X$, and suppose that $w\in \mathscr{C}^1(X,\mathbb{R})$ is a CLF in the sense of Definition def:clf. Consider a continuous $u:X_w\to U$ satisfying then, for all $x\in X_w$, it holds that $\xi_{x,u}(t)\in X_w$ for all $t\in \mathbb{R}_+$ and $\exists\;T_{x}\geq0$ such that $\xi_{x,u}(t)\in X_w(c),\, \forall t\geq T_

Figures (8)

  • Figure 1: Motivating example: A robot must navigate to and remain at targets $\mathcal{T}_1$, $\mathcal{T}_2$ or $\mathcal{T}_3$ as directed by an external environment which imposes respective modes $\mathcal{M}_1$, $\mathcal{M}_2$, and $\mathcal{M}_3$, while avoiding any collision with the walls $\mathcal{W}$ and with the door $\mathcal{D}$ (if it is closed).
  • Figure 2: Flowchart illustrating the overall algorithm given in Section \ref{['sec:ControlStrategy']}. Nodes , are the inputs and node is the output of our synthesis method. High-level and low-level synthesis steps are colored in dark and light grey, respectively, and discussed in the sections indicated at the arrows.
  • Figure 3: Illustration of a part of the initial parity game for the motivating example with $\text{Player}~1$ (squares) vertices and $\text{Player}~0$ (circles) vertices containing their priority in a black circle. A winning strategy template consists of unsafe edges indicated by red dotted arrows and co-live edges indicated by blue dashed arrows.
  • Figure 4: $X_a$ (region enclosed by red dotted line) and $X_e$ (region enclosed by blue dashed line) illustrate possible basins of attraction for the CLFs implementing the cRWAs $\Omega_a(d,e)$ (ensuring to reach $\mathcal{T}_1$ while avoiding only the walls) and $\Omega_e(d,e)$ (ensuring to reach $\mathcal{T}_1$ while avoiding walls and $\mathcal{T}_2$), respectively from \ref{['ex:RWAs']}.
  • Figure 5: Corresponding merged game for the initial game given in \ref{['fig:gamegraph']}, where labels of $\text{Player}~1$ vertices are empty sets.
  • ...and 3 more figures

Theorems & Definitions (48)

  • Definition 1
  • Definition 2
  • Lemma 1
  • Remark 1: CLFs-based Feedback design: Literature review
  • Lemma 2: spot_ltlsynt
  • Lemma 3: strategyTemplatereport
  • Definition 3
  • Proposition 1
  • Example 1
  • Definition 4
  • ...and 38 more