Zonotope-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 space and further to verify whether the LTL specification can be satisfied. Once the LTL specification can be satisfied, the next step is to design a controller to guarantee the satisfaction of the LTL specification for dynamic systems. Based on the verification of the LTL specification, an abstraction-based control design approach is proposed in this paper: a novel abstraction construction is developed first, then finite local abstract controllers are designed to achieve the LTL specification, and finally the designed abstract controllers are combined and refined as the controller for the original system. The proposed control strategy is illustrated via a numerical example from autonomous robots.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Zonotope-based Symbolic Controller Synthesis for Linear Temporal Logic Specifications
This paper studies the controller synthesis problem for nonlinear control systems under linear temporal logic (LTL) specifications using zonotope techniques. A local-to-global control strategy is proposed for the desired…
Reachability-based Control Synthesis under Signal Temporal Logic Specifications
In this paper, we investigate the controller design problem for linear disturbed systems under signal temporal logic (STL) specifications imposing both spatial and temporal constraints on system behavior. We first implem…
Formal Verification of Linear Temporal Logic Specifications Using Hybrid Zonotope-Based Reachability Analysis
In this paper, we introduce a hybrid zonotope-based approach for formally verifying the behavior of autonomous systems operating under Linear Temporal Logic (LTL) specifications. In particular, we formally verify the LTL…
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…
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 contributi…