Incremental Data-Driven Policy Synthesis via Game Abstractions

TL;DR

The paper addresses synthesizing correct-by-construction policies for unknown discrete-time stochastic systems with temporal logic objectives by building an incremental data-driven abstraction. It introduces a finite 2.5-player game graph constructed from data, with over- and under-approximations of reachable sets that refine monotonically as more data arrives, guaranteeing monotone expansion of the controller's winning region. A novel incremental game-solving approach based on a cofair coBüchi progress measure, augmented by compact DAG-like gadgets, enables efficient updates and warm-started solutions when new data arrives, and it is integrated with symbolic fixpoint solvers for fast initialization. End-to-end, the method yields significant runtime savings in updating winning regions and deriving controllers, offering scalable, online, data-driven policy synthesis for stochastic systems under complex temporal specifications.

Abstract

We address the synthesis of control policies for unknown discrete-time stochastic dynamical systems to satisfy temporal logic objectives. We present a data-driven, abstraction-based control framework that integrates online learning with novel incremental game-solving. Under appropriate continuity assumptions, our method abstracts the system dynamics into a finite stochastic (2.5-player) game graph derived from data. Given a requirement over time on this graph, we compute the winning region -- i.e., the set of initial states from which the objective is satisfiable -- in the resulting game, together with a corresponding control policy. Our main contribution is the construction of abstractions, winning regions and control policies incrementally, as data about the system dynamics accumulates. Concretely, our algorithm refines under- and over-approximations of reachable sets for each state-action pair as new data samples arrive. These refinements induce structural modifications in the game graph abstraction -- such as the addition or removal of nodes and edges -- which in turn modify the winning region. Crucially, we show that these updates are inherently monotonic: under-approximations can only grow, over-approximations can only shrink, and the winning region can only expand. We exploit this monotonicity by defining an objective-induced ranking function on the nodes of the abstract game that increases monotonically as new data samples are incorporated. These ranks underpin our novel incremental game-solving algorithm, which employs customized gadgets (DAG-like subgames) within a rank-lifting algorithm to efficiently update the winning region. Numerical case studies demonstrate significant computational savings compared to the baseline approach, which resolves the entire game from scratch whenever new data samples arrive.

Figures (9)

• Figure 1: Overview of (A) incremental synthesis, (B) motivating example, and (C) end-to-end data-driven synthesis. Our contributions ,, and , are highlighted in blue, along with the proven learning-induced monotonicity highlighted in red.
• Figure 2: Unknown function $f(x_*, u_*)$ (black), two noisy observations $x_1$, $x_2$ (small squares) and learned lower and upper bounds $\check{f}(x_*, u_*|\mathbf{D_2})$, $\hat{f}(x_*, u_*|\mathbf{D_2})$ (dashed).
• Figure 3: Gray areas indicate insufficient data and are initially excluded from the winning region. As new samples arrive from each room, they sequentially enter the winning region.
• Figure 4: Execution time of incremental lifting (blue dots) vs. full fixpoint recomputation (red ticks) across varying graph sizes: linear scale (left) and logarithmic scale (right).
• Figure 5: The figure represents the outgoing edges of a state $s$, and the subgame created thus, in the abstract fair game graph. The fair edges are denoted by dashed lines. Here, $m = m^{s,u}$ and a fair outgoing edge to the elliptic node represents a fair outgoing edge to each state $\underline{s} \in \underline{F}(s,u) \subseteq V_0$.

Theorems & Definitions (20)

• Theorem 1
• Theorem 2
• Theorem 3
• Theorem 4
• Corollary 1
• Theorem 5
• Lemma 1
• Theorem 5
• Theorem 5
• Theorem 5