Abstraction-Based Output-Feedback Control with State-Based Specifications

TL;DR

This paper presents a novel abstraction-based approach for designing output-feedback controllers for nonlinear systems with state-based specifications, extending existing methods to handle arbitrary predicate and observation maps and synthesizing controllers from LTL specifications.

Contribution

It generalizes feedback-refinement relations for output-feedback control to systems with arbitrary predicate and observation maps and introduces a new synthesis algorithm for controllers based on LTL specifications.

Findings

Developed a two-step synthesis process involving finite state abstraction and controller computation.

Extended feedback-refinement relations to more general systems with arbitrary predicate and observation maps.

Proposed an algorithm inspired by reactive synthesis under partial observation using bounded synthesis.

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.