Abstract

We consider the problem of controlling a discrete-time piecewise affine (PWA) system from a specification given as a Linear Temporal Logic (LTL) formula over linear predicates in its state variables. We present a computational framework for finding initial states and feedback control strategies guaranteeing the satisfaction of such a specification by all the trajectories of the closed loop system. Our solution is based on abstracting the system to a finite transition system and on controlling the abstraction from an LTL specification.

‚Äč