Specification-guided temporal logic control for stochastic systems: a multi-layered approach

TL;DR

The paper tackles provably correct control synthesis for stochastic systems under temporal logic specifications by proposing a specification-guided, multi-layered abstraction framework that blends discretization-based and discretization-free techniques. It introduces a multi-layered simulation relation with variable precision, develops robust dynamic programming for both homogeneous and heterogeneous layer configurations, and provides efficient switching strategies to balance accuracy and computation. The approach is validated on multiple case studies, showing improved robustness guarantees and reduced computation time compared with single-layer methods. The work advances practical correct-by-design synthesis for complex stochastic systems and lays groundwork for integrating heterogeneous abstractions into scalable verification and control pipelines.

Abstract

Designing controllers to satisfy temporal requirements has proven to be challenging for dynamical systems that are affected by uncertainty. This is mainly due to the states evolving in a continuous uncountable space, the stochastic evolution of the states, and infinite-horizon temporal requirements on the system evolution, all of which makes closed-form solutions generally inaccessible. A promising approach for designing provably correct controllers on such systems is to utilize the concept of abstraction, which is based on building simplified abstract models that can be used to approximate optimal controllers with provable closeness guarantees. The available abstraction-based methods are further divided into discretization-based approaches that build a finite abstract model by discretizing the continuous space of the system, and discretization-free approaches that work directly on the continuous state space without the need for building a finite space. To reduce the conservatism in the sub-optimality of the designed controller originating from the abstraction step, this paper develops an approach that naturally has the flexibility to combine different abstraction techniques from the aforementioned classes and to combine the same abstraction technique with different parameters. First, we develop a multi-layered discretization-based approach with variable precision by combining abstraction layers with different precision parameters. Then, we exploit the advantages of both classes of abstraction-based methods by extending this multi-layered approach guided by the specification to combinations of layers with respectively discretization-based and discretization-free abstractions. We achieve an efficient implementation that is less conservative and improves the computation time and memory usage. We illustrate the benefits of the proposed multi-layered approach on several case studies.

Figures (21)

• Figure 1: Example of an output space for a reach-avoid specification. The red area is the area to avoid, the green area is the goal region, and the black dot is the initial state $x(0)$.
• Figure 1: Cyclic DFA corresponding to the specification of the package delivery. Here, $\emptyset$ denotes the empty set, which means that all atomic propositions $p \in \mathrm{AP}$ are false.
• Figure 1: Multi-layered simulation relation $\boldsymbol{\mathscr{R}}$ consisting of two simulation relations $\mathscr{R}_1$ and $\mathscr{R}_2$. The edges are labeled with a lower bound on the probability that the transition occurs.
• Figure 1: Following respectively conditions 1 and 2 of Definition \ref{['def:switch']}, a possibility of switching action $s_{bf}$ from state $\hat{x}$ towards the state $x_w$ is shown in (a). A possibility of switching action $s_{fb}$ from state $x_w$ towards a subset $\hat{A}(x_w)$ is shown in (b).
• Figure 1: DFA $\mathcal{A}_{\phi_{park}}$ associated with specification $\phi_{park}= \lnot p_2 \mathbin{\sf U} p_1$. The initial, final, and sink state are denoted by respectively $q_0, q_f$, and $q_s$.

Theorems & Definitions (21)

• Definition 1: general Markov decision process (gMDP)
• Definition 2: scLTL syntax
• Definition 1: Coupling probability measures
• Definition 2: Multi-layered simulation relation
• Remark 1
• Remark 2
• Theorem 3
• Proof 1
• Lemma 4
• Proof 2