Unraveling tensor structures in correct-by-design controller synthesis
It addresses the scalability problem of formal controller synthesis for stochastic systems with temporal logic specifications, offering a method to alleviate exponential computational costs.
The paper tackles the curse of dimensionality in correct-by-design controller synthesis for stochastic systems by leveraging a tree structure in the Canonical Polyadic Decomposition of value functions, achieving significant computational reductions while providing provable probabilistic safety guarantees.
Formal safety guarantees on the synthesis of controllers for stochastic systems can be obtained using correct-by-design approaches. These approaches often use abstractions as finite-state Markov Decision Processes. As the state space of these MDPs grows, the curse of dimensionality makes the computational and memory cost of the probabilistic guarantees, quantified with dynamic programming, scale exponentially. In this work, we leverage decoupled dynamics and unravel, via dynamic programming operations, a tree structure in the Canonical Polyadic Decomposition (CPD) of the value functions. For discrete-time stochastic systems with syntactically co-safe linear temporal logic (scLTL) specifications, we provide provable probabilistic safety guarantees and significantly alleviate the computational burden. We provide an initial validation of the theoretical results on several typical case studies and showcase that the uncovered tree structure enables efficient reductions in the computational burden.