A powerful approach to control design with assurances is formal synthesis, e.g., [1]}, [2]}, [3]}, [4]}, [5]}. In this approach, the system specification is expressed in a formal language such as linear temporal logic (LTL) [6]}, and the system evolution is abstracted to a finite model–called abstraction–with a simulation relation. Then, using automated verification techniques, a controller is synthesized on the abstraction with performance guarantees. The controller and its guarantees are then refined onto the underlying system. These frameworks provide strong assurances but rely on accurate dynamics model to construct the abstraction, which may be unavailable for complex autonomous systems.
