CS 638: Formal Methods in Robotics and Automation
Units: 3-0-0-9
Overview
The term "formal methods" refers to mathematical techniques for verification and automatic synthesis of systems to ensure that the systems satisfy desirable properties given as specification. Formal methods are essential for building systems used for life-critical and mission critical applications. As robots are increasingly being used for such applications, use of formal methods has become critical for building robotic systems. In this course, we will study the recent development of formal methods based techniques for building software for robots. The course will cover basic concepts in formal methods and control theory and illustrate the potential of such techniques to be effective in the development of high quality robotic software.
Prerequisites
The course does not have any formal prerequisites. The students are expected to have mathematical maturity of the level of an undergraduate degree in engineering. However, some familiarity with finite state machines and ordinary differential equations, and programming experience will be helpful.
Course Contents:
- Basics of Verification: Finite State Machines, Linear Temporal Logic (LTL), Computation Tree Logic (CTL), Automata-Based LTL Model Checking, μ-Calculus Model Checking, Markov Decision Process, Probabilistic Computation Tree Logic (PCTL), Probabilistic Model Checking, Bisimulation Equivalence, Reactive Synthesis, Binary Decision Diagram, SAT and SMT Solvers
- Control Theory: Basics of Feedback Control Theory, Hybrid Systems, Discrete Abstraction of Hybrid Systems
- Motion Planning: Basics of Motion Planning, Sampling-Based Motion Planning, Feedback Motion Planning, Multi-Robot Motion Planning
- Formal Methods for Robotics: Motion Planning from LTL and μ-Calculus Specification, Motion Planning from Temporal Logic Specifications with Probabilistic Satisfaction Guarantees, Reactive Motion Plan Synthesis, Explaining Unsynthesizability for High-Level Robot Behaviors, Multi-Robot Motion Planning using SMT Solvers, Software Synthesis for Semi-Autonomous Systems
Books and References:
- C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.
- E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
- K. J. Astrom and R. M. Murray. Feedback Systems: An Introduction for Scientists and Engineers. Prince- ton University Press, 2009. http://www.cds.caltech.edu/~murray/amwiki/index.php/Main_Page.
- S. M. LaValle. Planning Algorithms. Cambridge University Press, 2006.
- Relevant research papers.
