COURSE

ROAS5120

Formal Verification and Control of Dynamical Systems

Systems Hub / Robotics and Autonomous Systems · 3 Credits

Formal methods originate from theoretical computer science and have been seamlessly integrated with dynamical systems. At its core, formal methods involve formulating specifications to form proof obligations, verifying that the systems indeed meet their specifications via algorithmic proof search, and designing systems to meet those obligations. This course bridges fundamental gaps between formal methods and control theory. It introduces fundamental theories and techniques of formal methods that apply broadly to various dynamical systems, such as robots, autonomous systems and cyber physical systems. Particularly, the following topics will be covered: symbolic system modeling, regular and omega-regular properties, linear temporal logic, model checking, system simulation and abstraction, game theoretic control synthesis and cutting-edge engineering applications.