Item

Abstract

We consider abstraction-based design of output-feedback controllers for
non-linear dynamical systems against specifications over state-based predicates
in linear-time temporal logic (LTL). In this context, our contribution is
two-fold: (I) we generalize feedback-refinement relations for abstraction-based
output-feedback control to systems with arbitrary predicate and observation
maps, and (II) we introduce a new algorithm for the synthesis of abstract
output-feedback controllers w.r.t. LTL specifications over unobservable
state-based predicates.
Our abstraction-based output-feedback controller synthesis algorithm consists
of two steps. First, we compute a finite state abstraction of the original
system using existing techniques. This process typically leads to an abstract
system with non-deterministic predicate and observation maps which are not
necessarily related to each other. Second, we introduce an algorithm to compute
an output-feedback controller for such abstract systems. Our algorithm is
inspired by reactive synthesis under partial observation and utilizes bounded
synthesis.