Infinite horizon safety controller synthesis through disjunctive polyhedral abstract interpretation

This paper presents a controller synthesis approach using disjunctive polyhedral abstract interpretation. Our approach synthesizes infinite time-horizon controllers for safety properties with discrete-time, linear plant model and a switching feedback controller that is suitable for time-triggered implementations. The core idea behind our approach is to perform an abstract interpretation over disjunctions of convex polyhedra to identify states that are potentially uncontrollable. Complementing this set yields the set of controllable states, starting from which, the safety property can be guaranteed by an appropriate controller feedback function. Since, a straightforward disjunctive domain is computationally inefficient, we present an abstract domain based on a state partitioning scheme that allows us to efficiently control the complexity of the intermediate representations. Next, we focus on the automatic generation of controller implementation from the abstract interpretation results. We show that a balanced tree approach can yield efficient controller code with guarantees on the worst-case execution time. Finally, we evaluate our approach on a suite of benchmarks, comparing different instantiations with related synthesis tools. The evaluation shows that our approach can successfully synthesize controller implementations for small to medium sized benchmarks.