Zonotope-based Symbolic Controller Synthesis for Linear Temporal Logic Specifications

TL;DR

This paper tackles controller synthesis for nonlinear systems under LTL specifications by introducing a zonotope-based covering of the state space that permits overlapping cells and neighbor intersections. A graph-based realization verification then decomposes the global accepting path into a sequence of finite local regions, enabling a local-to-global abstraction-based synthesis where each cell has its own symbolic model and equivalence relation. The approach yields a robust, scalable framework that combines local abstractions to ensure global LTL satisfaction, demonstrated via a mobile robot path-planning example. The method reduces conservatism and computation relative to global discretization by exploiting zonotope geometry and cell-wise refinements, with clear pathways for extension to multi-robot systems and other temporal logics.

Abstract

This paper studies the controller synthesis problem for nonlinear control systems under linear temporal logic (LTL) specifications using zonotope techniques. A local-to-global control strategy is proposed for the desired specification expressed as an LTL formula. First, a novel approach is developed to divide the state space into finite zonotopes and constrained zonotopes, which are called cells and allowed to intersect with the neighbor cells. Second, from the intersection relation, a graph among all cells is generated to verify the realization of the accepting path for the LTL formula. The realization verification determines if there is a need for the control design, and also results in finite local LTL formulas. Third, once the accepting path is realized, a novel abstraction-based method is derived for the controller design. In particular, we only focus on the cells from the realization verification and approximate each cell thanks to properties of zonotopes. Based on local symbolic models and local LTL formulas, an iterative synthesis algorithm is proposed to design all local abstract controllers, whose existence and combination establish the global controller for the LTL formula. Finally, the proposed framework is illustrated via a path planning problem of mobile robots.

Figures (11)

• Figure 1: The state space of the robot in Example 1. The four regions of interest are denoted as $\mathbbmss{R}(\pi_{0}), \mathbbmss{R}(\pi_{1}), \mathbbmss{R}(\pi_{2}), \mathbbmss{R}(\pi_{3})$ with the propositions $\pi_{0}, \pi_{1}, \pi_{2}, \pi_{3}$, and the three obstacles are $\mathbb{O}_{1}, \mathbb{O}_{2}, \mathbb{O}_{3}$.
• Figure 2: Illustration of the generation of zonotopes in different cases. (a) $N=2<3$: the generated zonotopes are two segments and thus not well-constructed. (b) $N=3$: three zonotopes are generated and overlapped. (c) $N=4$ and each center connects with 2 neighbor centers: four zonotopes are generated but not overlapped. (d) $N=4$ and each center connects with 3 neighbor centers: four zonotopes are generated and overlapped.
• Figure 3: Illustration of the generation of constrained zonotopes for the case in Fig. \ref{['fig-2']}(d). (i) Illustration of line 7 in Algorithm \ref{['alg-2']}. The boundaries of four zonotopes are lines in different colors, and $\mathbb{H}_{1}=\{\mathsf{h}_{1}, \ldots, \mathsf{h}_{20}\}$. (ii) Illustration of line 8, and $\mathbb{H}=\{\mathsf{h}_{1}, \ldots, \mathsf{h}_{16}\}$. (iii)-(iv) Illustration of different ways to lines 9-10. In (iii), the set $\mathbb{S}$ has 8 triangle regions, which are used to construct $M=8$ constrained zonotopes. In (iv), the set $\mathbb{S}$ has 4 regions, which are used to construct $M=4$ constrained zonotopes.
• Figure 4: Illustration of Algorithm \ref{['alg-3']} via Fig. \ref{['fig-3']}(iii). (a) The cover of the state space $\mathbb{X}\subset\mathbb{R}^{2}$, and $\mathbb{O}_{3}$ in Fig. \ref{['fig-1']} is removed here. (b) The graph $\mathcal{G}=(\mathcal{V}, \mathcal{E})$ with $\mathcal{V}=\{\mathsf{v}_{1}, \ldots, \mathsf{v}_{12}\}$ and $\mathcal{E}$ from the adjacency matrix $A$.
• Figure 5: Illustration of the state space in Fig. \ref{['fig-4']}(a). For each $i\in\{0, 1, 2, 3\}$, the light green region is included in $\mathbbmss{R}(\pi_{i})$ while not in $\mathbbmss{R}(\pi^{\varepsilon}_{i})$. For each $j\in\{1, 2\}$, $\mathbf{O}_{j}=\mathbf{E}_{\varepsilon}(\mathbb{O}_{j})$ includes both dark and light grey regions.

Theorems & Definitions (24)

• Lemma 1: Scott2016constrained
• Definition 1: Girard2007approximation
• Definition 2: Girard2007approximation
• Definition 3: Reissig2017feedback
• Definition 4: Girard2012controller
• Definition 5: Clarke2018handbook
• Definition 6
• Example 1
• Definition 7
• Remark 1