Specification-guided controller synthesis for linear systems and safe linear-time temporal logic

In this paper we present and analyze a novel algorithm to synthesize controllers enforcing linear temporal logic speci-fications on discrete-time linear systems. The central step within this approach is the computation of the maximal con-trolled invariant set contained in a possibly non-convex safe set. Although it is known how to compute approximations of maximal controlled invariant sets, its exact computation remains an open problem. We provide an algorithm which computes a controlled invariant set that is guaranteed to be an under-approximation of the maximal controlled invari-ant set. Moreover, we guarantee that our approximation is at least as good as any invariant set whose distance to the boundary of the safe set is lower bounded. The proposed algorithm is founded on the notion of sets adapted to th