ABSTRACT
This chapter is a collection of case studies of formal methods for solving real-world control synthesis problems. The main theme is motion planning and control in robotics. A variety of applications are included, such as parallel parking, motion planning in static and dynamic environments for mobile robots and manipulators, and reactive walking control of humanoid robots. These examples demonstrate the capability of formal methods for handling complex specifications, dynamics as well as environments, which are common factors in the field of robotics. The first few use cases explore the application of formal methods beyond robotics, and the control of power electronics devices and jet engines are discussed. Last but not least, it also gives a brief performance evaluation of the formal methods presented in this book based on the computational results from the presented applications.
