Correct-by-Design Control Synthesis of Stochastic Multi-agent Systems: a Robust Tensor-based Solution

TL;DR

This paper introduces a tensor-based, abstraction-driven control synthesis framework for stochastic multi-agent systems, ensuring probabilistic correctness and scalability in verifying temporal logic specifications.

Contribution

It presents a novel tensor decomposition approach to scalable dynamic programming for stochastic systems with formal guarantees.

Findings

Tensor decomposition enables scalable dynamic programming.

Framework provides probabilistic guarantees for temporal logic.

Validated on continuous-state linear stochastic systems.

Abstract

Discrete-time stochastic systems with continuous spaces are hard to verify and control, even with MDP abstractions due to the curse of dimensionality. We propose an abstraction-based framework with robust dynamic programming mappings that deliver control strategies with provable lower bounds on temporal-logic satisfaction, quantified via approximate stochastic simulation relations. Exploiting decoupled dynamics, we reveal a Canonical Polyadic Decomposition tensor structure in value functions that makes dynamic programming scalable. The proposed method provides correct-by-design probabilistic guarantees for temporal logic specifications. We validate our results on continuous-state linear stochastic systems.