Compressing Correct-by-Design Synthesis for Stochastic Homogeneous Multi-Agent Systems with Counting LTL
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915923787513856 |
|---|---|
| author | Qiu, Xinyuan Wang, Ruohan Liu, Siyuan Haesaert, Sofie |
| author_facet | Qiu, Xinyuan Wang, Ruohan Liu, Siyuan Haesaert, Sofie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_06868 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Compressing Correct-by-Design Synthesis for Stochastic Homogeneous Multi-Agent Systems with Counting LTL Qiu, Xinyuan Wang, Ruohan Liu, Siyuan Haesaert, Sofie Systems and Control 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. |
| title | Compressing Correct-by-Design Synthesis for Stochastic Homogeneous Multi-Agent Systems with Counting LTL |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2604.06868 |