Spatiotemporal Tubes based Controller Synthesis against Omega-Regular Specifications for Unknown Systems

Abstract

This paper provides a discretization-free solution to the synthesis of approx-imation-free closed-form controllers for unknown nonlinear systems to enforce complex properties expressed by $ω$-regular languages, as recognized by Non-deterministic Büchi Automata (NBA). In order to solve this problem, we first decompose NBA into a sequence of reach-avoid problems, which are solved using the Spatiotemporal Tubes (STT) approach. Controllers for each reach-avoid task are then integrated into a hybrid policy that ensures the fulfillment of the desired $ω$-regular properties. We validate our method through omnidirectional robot navigation and manipulator control case studies.