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 (omega$$ \omega $$)-regular languages and equivalently recognized by nondeterministic Buchi 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 (omega$$ \omega $$)-regular property. We demonstrate the effectiveness of the proposed results on room temperature control and mobile robot motion control case studies.