Scaling up controller synthesis for linear systems and safety specifications

In this paper we revisit the problem of automatically synthesizing control software enforcing formal specifications given in temporal logic. Existing approaches to solve this problem rely on the explicit or implicit construction of finite abstractions of control systems. Unfortunately, the existing abstraction techniques do not scale beyond a small number of state variables. The objective of this paper is to scale up the construction of such abstractions by focusing on linear control systems and safety specifications. In this more restricted scenario the controller synthesis problem can be reduced to the computation of control invariant subsets. Hence, we focus on the control invariance problem and propose a computational technique exploiting controllability. We illustrate the proposed methods on several synthetic examples illustrating the computational limits of our algorithm.