Correctness and Safety in Planning and Control via State-Space Partitions and Barrier Functions

Autonomous systems have become increasingly prevalent in various industries, ranging from household cleaning robots to line inspection drones and copilot vehicles. Ensuring real-time safety is becoming a critical issue when the environment is rapidly changing. Moreover, most of these autonomous systems are still pale in satisfying complex nested temporal logic tasks. Possible solutions to these problems include correct-by-construction and safe-by-construction planning and control algorithms, since they can provide theoretical correctness and safety guarantees for autonomous systems. This thesis proposes several techniques for developing correct- and safe-by-construction planning and control algorithms, exploring both theoretical guarantees and practical implementations. One missing component of the existing correct-by-construction algorithms is that abstraction algorithms, which are essential for automaton-based task planning, are largely limited to linear systems associated with polytopic partitionings of the state space. State-space partitioning and control problem for systems on a curved manifold is relatively unexplored. The first part of the thesis is devoted to alleviating this problem. In particular, we consider $SO(3)$ and $\mathbb{S}^2 $, the two most commonly encountered manifolds in mechanical systems, and propose several approaches to address the partitioning and control problem, which in principle could be generalized to other manifolds. In the second part of the thesis, various theoretical and practical issues related to the emerging control barrier functions (CBFs) approach are investigated. CBFs provides a modular, easy-to-implement framework to render an existing control scheme safe.It is known that CBF for system safety can be viewed as an extension of the classic control Lyapunov function (CLF) approach for system stabilization. Despite their similarity, CBFs have many unique research problems of their own. In this part, we will investigate the construction and theoretical guarantees for ...