Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Unraveling tensor structures in correct-by-design controller synthesis

Ruohan Wang, Zhiyong Sun, Sofie Haesaert

TL;DR

The paper addresses the curse of dimensionality in correct-by-design controller synthesis for stochastic systems with temporal logic specifications. It leverages decoupled dynamics to represent value functions with a low-rank CPD tensor and introduces a tree-based value iteration that is guided by a DFA, enabling pruning while preserving probabilistic safety guarantees. The key contribution is a provable bound on CPD rank growth and an efficient, scalable algorithm that combines DFA-informed operators with tensor trees. Case studies demonstrate substantial memory and time savings, achieving near-exact results in 2D and scalable performance up to higher dimensions, which has practical implications for safe control in large-scale, uncertain systems.

Abstract

Formal safety guarantees on the synthesis of controllers for stochastic systems can be obtained using correct-by-design approaches. These approaches often use abstractions as finite-state Markov Decision Processes. As the state space of these MDPs grows, the curse of dimensionality makes the computational and memory cost of the probabilistic guarantees, quantified with dynamic programming, scale exponentially. In this work, we leverage decoupled dynamics and unravel, via dynamic programming operations, a tree structure in the Canonical Polyadic Decomposition (CPD) of the value functions. For discrete-time stochastic systems with syntactically co-safe linear temporal logic (scLTL) specifications, we provide provable probabilistic safety guarantees and significantly alleviate the computational burden. We provide an initial validation of the theoretical results on several typical case studies and showcase that the uncovered tree structure enables efficient reductions in the computational burden.

Unraveling tensor structures in correct-by-design controller synthesis

TL;DR

The paper addresses the curse of dimensionality in correct-by-design controller synthesis for stochastic systems with temporal logic specifications. It leverages decoupled dynamics to represent value functions with a low-rank CPD tensor and introduces a tree-based value iteration that is guided by a DFA, enabling pruning while preserving probabilistic safety guarantees. The key contribution is a provable bound on CPD rank growth and an efficient, scalable algorithm that combines DFA-informed operators with tensor trees. Case studies demonstrate substantial memory and time savings, achieving near-exact results in 2D and scalable performance up to higher dimensions, which has practical implications for safe control in large-scale, uncertain systems.

Abstract

Formal safety guarantees on the synthesis of controllers for stochastic systems can be obtained using correct-by-design approaches. These approaches often use abstractions as finite-state Markov Decision Processes. As the state space of these MDPs grows, the curse of dimensionality makes the computational and memory cost of the probabilistic guarantees, quantified with dynamic programming, scale exponentially. In this work, we leverage decoupled dynamics and unravel, via dynamic programming operations, a tree structure in the Canonical Polyadic Decomposition (CPD) of the value functions. For discrete-time stochastic systems with syntactically co-safe linear temporal logic (scLTL) specifications, we provide provable probabilistic safety guarantees and significantly alleviate the computational burden. We provide an initial validation of the theoretical results on several typical case studies and showcase that the uncovered tree structure enables efficient reductions in the computational burden.

Paper Structure

This paper contains 17 sections, 9 theorems, 67 equations, 8 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries and problem setup
  3. Models: Markov decision processes (MDP)
  4. Specification
  5. Problem setup
  6. Value iteration for temporal logic specifications
  7. scLTL as a probabilistic reach-avoid problem
  8. DFA-informed operators
  9. Tensor representation of value function
  10. Tree-based value iterations
  11. Trees, values, and tensors
  12. Efficient optimal value iteration
  13. Case studies
  14. Two dimensional case
  15. Four dimensional case
  16. ...and 2 more sections

Key Result

Proposition 1

For a given policy $\boldsymbol{\pi}=\{\pi[k]|k=0,1,\ldots,N-1\}$ with $\pi[k]:\mathbb{S} \times Q \rightarrow \mathbb{A}$, the satisfaction probability within time horizon $N$ for specification $\phi$ of system $\mathbf{M}$ is defined as with $\bar{q}_0= \tau_{\mathcal{A}}(q_0,L(s_0))$ and computed iteratively as in eq:vi_dfa, and initialized as in eq:value_function_initialization_tensor.

Figures (8)

  • Figure 1: Left: DFA ($q_s$ denotes $q_{\text{sink}}$ for simplicity), right: state space labeled by $l$ or $\alpha$.
  • Figure 2: The computation of the value function based on the operators $\mathbf T_\alpha$\ref{['eq:OperatorPi']} follows the structure of the DFA. The operators that are used to computed $\mathcal{V}_{q_0}$ are depicted on the edges of the DFA.
  • Figure 3: Illustration of order-3 tensor with its Canonical Polyadic Decomposition
  • Figure 4: Tree expanded iteratively based on Alg. \ref{['alg:sofie']} as $\mathcal{G}_0$, $\mathcal{G}_1$, $\mathcal{G}_2$, and $\mathcal{G}_3$. Examples: $\mathcal{G}_0$ with $\mathrm{N}_0=\{1\},$$\mathcal{G}_1$ with $\mathrm{N}_1=\{1,2,3\}$ and $\mathcal{E}_1=\{(1,\alpha,2),(1,\alpha,3)\}$.
  • Figure 5: Satisfaction probability error of rank-1 tree-based value iteration. Error is computed with respect to using exact value iteration.
  • ...and 3 more figures

Theorems & Definitions (21)

  • Definition 1: MDP
  • Definition 2: Markov policy $\boldsymbol{\pi}$
  • Definition 3: scLTL syntax
  • Remark 1
  • Definition 4: DFA
  • Proposition 1: scLTL satisfaction
  • Proposition 2: Optimal scLTL satisfaction
  • Proposition 3
  • Example 1
  • Lemma 1: Equivalence of DFA-informed operator
  • ...and 11 more