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.
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.
Class Attendance - 5%
Homework Assignments - 15%
Project - 30%
Mid-Semester Examination - 30%
End-Semester Examination - 20%
Homework Assignments
Assignment 1 (Released: January 20, 2020; Deadline: February 9, 2020)
Assignment 2 (Released: February 29, 2020; Deadline: March 15, 2020)
Assignment 3 (Released: March 16, 2020; Deadline: April 5, 2020)
Mid-Semester Examination
February 19, 2020 (Wednesday) 1:00 pm to 3:00 pm in RM101
Final Examination
April 27, 2020 (Monday) 4:00 pm to 7:00 pm at RM101
| Lecture | Date | Topic | References |
| 1 | January 6, 2020 (Monday) | Introduction to the course, Transition Systems | [BYG17, Ch-1] |
| 2 | January 8, 2020 (Wednesday) | Simulation and Bisimulation | [BYG17 Ch-1] |
| 3 | January 13, 2020 (Monday) | Linear Temporal Logic | [BYG17 Ch-2], [BK08] |
| 4 | January 15, 2020 (Wednesday) | Temporal Logic to Automata | [BYG17 Ch-2], [BK08] |
| 5 | January 20, 2020 (Monday) | Model Checking | [BYG17 Ch-3] |
| 6 | January 22, 2020 (Wednesday) | Largest Finite Satisfying Region | [BYG17 Ch-4] |
| 7 | January 27, 2020 (Monday) | Largest Finite Satisfying Region | [BYG17 Ch-4] |
| 8 | January 29, 2020 (Wednesday) | Finite Temporal Logic Control | [BYG17 Ch-5] |
| 9 | February 3, 2020 (Monday) | Finite Temporal Logic Control | [BYG17 Ch-5] |
| 10 | February 5, 2020 (Wednesday) | Discrete-Time Dynamical Systems | [BYG17 Ch-6], [AM09] |
| 11 | February 10, 2020 (Monday) | Largest Satisfying Region | [BYG17 Ch-7] |
| 12 | February 12, 2020 (Wednesday) | Parameter Synthesis, Temporal Logic Based COntrol | [BYG17 Ch-8, Ch-9] |
| -- | February 17, 2020 (Monday) | Mid-Semester Examination | |
| -- | February 19, 2020 (Wednesday) | Mid-Semester Examination | |
| 13 | February 24, 2020 (Monday) | Review of the Questions of Mid-Semester Examination | - |
| 14 | February 26, 2020 (Wednesday) | SAT and SMT Solver | [dMB08], [NOT06], |
| 15 | February 29, 2020 (Saturday) | SAT and SMT-Based Temporal Logic Motion Planning | [SRK+14], [SRK+16] |
| 16 | March 2, 2020 (Monday) | Graph-Based Temporal Logic Motion Planning | [KhS18] |
| 17 | March 4, 2020 (Wednesday) | Sampling-Based Motion Planning, Reactive Motion Planning | [Lav06], [KFP09] |
| -- | March 9, 2020 (Monday) | Mid-Semester Recess | |
| -- | March 11, 2020 (Wednesday) | Mid-Semester Recess | |
| 18 | March 16, 2020 (Monday) | Student Presentations | - |
| 19 | March 18, 2020 (Wednesday) | Student Presentations | - |
| 20 | March 23, 2020 (Monday) | Student Presentations | - |
| 21 | March 25, 2020 (Wednesday) | Student Presentations | - |
| 22 | March 30, 2020 (Monday) | Student Presentations | - |
| 23 | April 1, 2020 (Wednesday) | Student Presentations | - |
| -- | April 6, 2020 (Monday) | No Class: Mahavir Jayanti | |
| 24 | April 8, 2020 (Wednesday) | Student Presentations | - |
| 25 | April 13, 2020 (Monday) | Student Presentations | - |
| 26 | April 15, 2020 (Wednesday) | Course Wrap-up | - |
[BYG17] Calin Belta, Boyan Yordanov, Ebru Aydin Gol: Formal Methods for Discrete-Time Dynamical Systems. Springer, 2017.
[AM09] K. J. Astrom and R. M. Murray. Feedback Systems: An Introduction for Scientists and Engineers. Prince- ton University Press, 2009.
[BK08] C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.
[dMB08] L. M. de Moura and N. Bjorner. Z3: An efficient smt solver. In TACAS, pages 337-340, 2008.
[KFP09] H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. Temporal-logic-based reactive mission and motion
planning. IEEE Transactions on Robotics, 25(6):1370-1381, 2009.
[LaV06] S. M. LaValle. Planning Algorithms. Cambridge University Press, 2006.
[NOT06] R. Nieuwenhuis, A. Oliveras, C. Tinelli. Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). J. ACM 53(6): 937-977, 2006.
[SRK+14] I. Saha, R. Ramaithitima, V. Kumar, G. J. Pappas, and S. A. Seshia. Automated composition of motion primitives for multi-robot systems from safe LTL specifications. In IROS, pages 1525-1532, 2014.
[SRK+16] I. Saha, R. Ramaithitima, V. Kumar, G. J. Pappas, and S. A. Seshia. Implan: Scalable Incremental Motion Planning for Multi-Robot Systems. In ICCPS, pages 1525-1532, 2016.
[KhS18] Danish Khalidi, Indranil Saha:
T* : A Heuristic Search Based Algorithm for Motion Planning with Temporal Goals. CoRR abs/1809.05817 (2018)