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.
Homework Assignments - 20%
Mid-Semester Examination - 30%
Literature Review and Class Presentation - 40%
Class Attendance - 10%
Mid-Semester Examination - Feb 23; 1-3 pm; Venue: KD101
Book Chapter Presentations - March 25, 27, April 1, 3, 8, 10, 15; Venue: KD101
Book Chapter Submission Deadline - April 18
| Lecture | Date | Topic | References |
| 1 | January 7, 2019 (Monday) | Introduction to the course, Transition Systems | [BYG17, Ch-1] |
| 2 | January 9, 2019 (Wednesday) | Simulation and Bisimulation | [BYG17 Ch-1] |
| 3 | January 12, 2019 (Saturday) | Linear Temporal Logic | [BYG17 Ch-2], [BK08] |
| 4 | January 14, 2019 (Monday) | Temporal Logic to Automata | [BYG17 Ch-2], [BK08] |
| 5 | January 16, 2019 (Wednesday) | Model Checking | [BYG17 Ch-3] |
| 6 | January 21, 2019 (Monday) | Largest Finite Satisfying Region | [BYG17 Ch-4] |
| 7 | January 23, 2019 (Wednesday) | Largest Finite Satisfying Region | [BYG17 Ch-4] |
| 8 | January 28, 2019 (Monday) | Finite Temporal Logic Control | [BYG17 Ch-5] |
| 9 | January 30, 2019 (Wednesday) | Finite Temporal Logic Control | [BYG17 Ch-5] |
| 10 | February 4, 2019 (Monday) | Discrete-Time Dynamical Systems | [BYG17 Ch-6], [AM09] |
| 11 | February 6, 2019 (Wednesday) | Largest Satisfying Region | [BYG17 Ch-7] |
| 12 | February 11, 2019 (Monday) | Parameter Synthesis | [BYG17 Ch-8] |
| 13 | February 13, 2019 (Wednesday) | Temporal Logic Control | [BYG17 Ch-9] |
| -- | February 18, 2019 (Monday) | Mid-Semester Examination | |
| -- | February 20, 2019 (Wednesday) | Mid-Semester Examination | |
| 14 | February 25, 2019 (Monday) | SAT and SMT Solver | [dMB08], [NOT06], |
| 15 | February 27, 2019 (Wednesday) | SMT-Based Motion Planning | [SRK+14], [SRK+16] |
| -- | March 4, 2019 (Monday) | No Class: Maha Sivaratri | |
| 16 | March 6, 2019 (Wednesday) | Reactive Motion Planning | [PPS06] |
| 17 | March 11, 2019 (Monday) | SMT-Based Coverage Planning (Ratijit) | [DS18] |
| 18 | March 13, 2019 (Wednesday) | Graph Based LTL Motion Planning (Dhaval) | [KhS18] |
| -- | March 18, 2019 (Monday) | Mid-Semester Recess | |
| -- | April 20, 2019 (Wednesday) | Mid-Semester Recess | |
| 19 | March 25, 2019 (Monday) | Student Presentations 1a and 1b | - |
| 20 | March 27, 2019 (Wednesday) | Student Presentations 2a and 2b | - |
| 21 | April 1, 2019 (Monday) | Student Presentation 3a and 3b | - |
| 22 | April 3, 2019 (Wednesday) | Student Presentations 4a and 4b | - |
| 23 | April 8, 2019 (Monday) | Student Presentations 5a and 5b | - |
| 24 | April 10, 2019 (Wednesday) | Student Presentations 6a and 6b | - |
| 25 | April 15, 2019 (Monday) | Student Presentations 7a, 7b, 7c | - |
| -- | April 17, 2019 (Wednesday) | No Class: Mahavir Jayanti | |
[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. Bjørner. 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.
[PPS06] N. Piterman, A. Pnueli, and Y. Sa'ar. Synthesis of reactive(1) designs. In VMCAI, pages 364-380, 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)
[KuS18] Tanmoy Kundu, Indranil Saha:
Charging Station Placement for Indoor Robotic Applications. ICRA 2018: 3029-3036.
[DS18] Sankar Narayan Das, Indranil Saha:
Rhocop: receding horizon multi-robot coverage. ICCPS 2018: 174-185.