Abstraction-Based Output-Feedback Control with State-Based Specifications
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow…
A Framework for Output-Feedback Symbolic Control
Symbolic control is an abstraction-based controller synthesis approach that provides, algorithmically, certifiable-by-construction controllers for cyber-physical systems. Symbolic control approaches usually assume that f…
NNSynth: Neural Network Guided Abstraction-Based Controller Synthesis for Stochastic Systems
In this paper, we introduce NNSynth, a new framework that uses machine learning techniques to guide the design of abstraction-based controllers with correctness guarantees. NNSynth utilizes neural networks (NNs) to guide…
Imitation LearningZonotope-based Controller Synthesis for LTL Specifications
This paper studies the controller synthesis problem for Linear Temporal Logic (LTL) specifications using (constrained) zonotope techniques. First, we implement (constrained) zonotope techniques to partition the state spa…
Approximately symbolic models for a class of continuous-time nonlinear systems
Discrete abstractions have become a standard approach to assist control synthesis under complex specifications. Most techniques for the construction of discrete abstractions are based on sampling of both the state and ti…