Correct-by-Design Control Synthesis of Stochastic Multi-agent Systems: a Robust Tensor-based Solution
Ruohan Wang, Siyuan Liu, Zhiyong Sun, Sofie Haesaert
连续空间的离散时间随机系统很难验证和控制,即使由于尺寸性的诅咒而具有MDP抽象。 我们提出了一个基于抽象的框架,具有强大的动态编程映射,在时间逻辑满意度方面提供具有可证明下限的控制策略,并通过近似随机模拟关系进行量化。 利用解耦动力学,我们揭示了价值函数中的 Canonical Polyadic 分解张量结构,使动态编程具有可扩展性。 提议的方法为时间逻辑规范提供了按设计的正确概率保证。 我们在连续状态线性随机系统上验证我们的结果。
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 tha...