Controller Synthesis against Omega-Regular Specifications: A
Funnel-based Control Approach
The paper focuses on the problem of formal synthesis of controllers for
control-affine nonlinear systems against complex properties. Our goal is
to design a closed-form control policy that guarantees the satisfaction
of complex properties that are expressed using ( ω)-regular
languages and equivalently recognized by Non-deterministic Büchi
Automata (NBA). We propose leveraging a funnel-based control approach to
provide a closed-form solution to the problem. Our approach decomposes
the specification represented by NBA into a sequence of reachability
problems which we solve using a funnel-based control approach.
Controllers associated with each reachability problem are then combined
to design a hybrid control policy enforcing the desired (
ω)-regular property. We demonstrate the effectiveness of the
proposed results on room temperature control and mobile robot motion
control case studies.