Guaranteed Memory Reduction in Synthesis of Correct-by-design Invariance Controllers

Formal methods for analysis of dynamical systems through construction of finite symbolic abstractions have attracted significant interest as they allow solving complex control problems in a fully automated fashion. Nevertheless, their practical application is currently limited by the fact that they require enormous memory resources. We present a novel algorithm for solution of invariance problems within abstraction-based framework, which guarantees large storage reduction and fully applies to general non-linear plants. We also show that, in practice, the algorithm is faster compared to other methods.