Abstraction-Based Output-Feedback Control with State-Based Specifications
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.
Cite
@article{arxiv.2104.10974,
title = {Abstraction-Based Output-Feedback Control with State-Based Specifications},
author = {Anne-Kathrin Schmuck and Mehrdad Zareian},
journal= {arXiv preprint arXiv:2104.10974},
year = {2021}
}