Compressing Correct-by-Design Synthesis for Stochastic Homogeneous Multi-Agent Systems with Counting LTL

TL;DR

This paper introduces a scalable method for synthesizing correct-by-design controllers for large homogeneous stochastic multi-agent systems under counting LTL specifications, leveraging tensor decomposition and dual-tree value iteration.

Contribution

It proposes a novel tensor decomposition approach and a dual-tree value iteration framework to efficiently handle complex specifications and large-scale systems.

Findings

The method reduces computational costs compared to traditional finite abstraction approaches.

Numerical results show improved scalability and effectiveness for complex specifications.

The approach successfully synthesizes controllers for large homogeneous stochastic multi-agent systems.

Abstract

Correct-by-design synthesis provides a principled framework for establishing formal safety guarantees for stochastic multi-agent systems (MAS). However, conventional approaches based on finite abstractions often incur prohibitive computational costs as the number of agents and the complexity of temporal logic specifications increase. In this work, we study homogeneous stochastic MAS under counting linear temporal logic (cLTL) specifications, and show that the corresponding satisfaction probability admits a structured tensor decomposition via leveraging deterministic finite automata (DFA). Building on this structure, we develop a dual-tree-based value iteration framework that reduces redundant computation in the process of dynamic programming. Numerical results demonstrate the proposed approach's effectiveness and scalability for complex specifications and large-scale MAS.