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.

Hydrobatic Autonomous Underwater Vehicles (AUVs) can be efficient in range and speed, as well as agile in maneuvering. They can be beneficial in scenarios such as obstacle-avoidance, inspections, docking, and under-ice operations. However, such AUVs are underactuated systems - this means exploiting the system dynamics is key to achieving elegant hydrobatic maneuvers with minimum controls. This paper explores the use of Model Predictive Control (MPC) techniques to control underactuated AUVs in hydrobatic maneuvers and presents new simulation and experimental results with the small and hydrobatic SAM AUV. Simulations are performed using nonlinear MPC (NMPC) on the full AUV system to provide optimal control policies for several hydrobatic maneuvers in Matlab/Simulink. For implementation on AUV hardware in ROS, a linear time varying MPC (LTV-MPC) is derived from the nonlinear model to enable real-time control. In simulations, NMPC and LTV-MPC shows promising results to offer much more efficient control strategies than what can be obtained with PID and LQR based controllers in terms of rise-time, overshoot, steady-state error and robustness. The LTV-MPC shows satisfactory real-time performance in experimental validation. The paper further also demonstrates experimentally that LTV-MPC can be run real-time on the AUV in performing hydrobatic maneouvers.