Controller synthesis for linear systems and safe linear-time temporal logic
Abstract:
In this talk I will describe a new approach to synthesize control software enforcing safe linear-time temporal logic requirements on linear control systems. Contrary to most controller synthesis approaches enforcing temporal logic specifications on control systems, we do not compute a discrete abstraction of the continuous dynamics. Instead, we rely on the computation of maximal controlled invariant sets. I will present an algorithm to compute a controlled invariant set that is guaranteed to be an under-approximation of the maximal controlled invariant set that can be rendered as tight as required. Our preliminary implementation handles up to five continuous dimensions and specifications containing up to 160 predicates defined as polytopes in about 30 minutes with less than 1GB memory.