CS638: Formal Methods for Robotics and Automation

Winter 2019 (January 4, 2019 - April 18, 2019)

Lecture Hours: Monday and Wednesday 2 pm to 3:30 pm
Office Hour: Friday 4:00 pm to 5:00 pm

Lecture Venue: KD101

Instructor: Indranil Saha

Teaching Assistants:
Tanmoy Kundu (Email: tanmoy[at]cse[dot]iitk[dot]ac[dot]in)
Ratijit Mitra (Email: ratijit[at]cse[dot]iitk[dot]ac[dot]in)
Dhaval Gujarathi (Email: gdhaval[at]cse[dot]iitk[dot]ac[dot]in)


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.


Grading Policy

Homework Assignments - 20%
Mid-Semester Examination - 30%
Literature Review and Class Presentation - 40%
Class Attendance - 10%


Exam Schedule and Deadlines

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 Schedule


Lecture Date Topic References
1January 7, 2019 (Monday)Introduction to the course, Transition Systems[BYG17, Ch-1]
2January 9, 2019 (Wednesday)Simulation and Bisimulation [BYG17 Ch-1]
3January 12, 2019 (Saturday)Linear Temporal Logic[BYG17 Ch-2], [BK08]
4January 14, 2019 (Monday)Temporal Logic to Automata[BYG17 Ch-2], [BK08]
5January 16, 2019 (Wednesday)Model Checking[BYG17 Ch-3]
6January 21, 2019 (Monday)Largest Finite Satisfying Region[BYG17 Ch-4]
7January 23, 2019 (Wednesday)Largest Finite Satisfying Region[BYG17 Ch-4]
8January 28, 2019 (Monday) Finite Temporal Logic Control[BYG17 Ch-5]
9January 30, 2019 (Wednesday)Finite Temporal Logic Control[BYG17 Ch-5]
10February 4, 2019 (Monday)Discrete-Time Dynamical Systems[BYG17 Ch-6], [AM09]
11February 6, 2019 (Wednesday)Largest Satisfying Region[BYG17 Ch-7]
12 February 11, 2019 (Monday)Parameter Synthesis[BYG17 Ch-8]
13February 13, 2019 (Wednesday)Temporal Logic Control [BYG17 Ch-9]
--February 18, 2019 (Monday) Mid-Semester Examination
--February 20, 2019 (Wednesday) Mid-Semester Examination
14February 25, 2019 (Monday)SAT and SMT Solver [dMB08], [NOT06],
15February 27, 2019 (Wednesday)SMT-Based Motion Planning[SRK+14], [SRK+16]
--March 4, 2019 (Monday) No Class: Maha Sivaratri
16March 6, 2019 (Wednesday)Reactive Motion Planning[PPS06]
17March 11, 2019 (Monday)SMT-Based Coverage Planning (Ratijit) [DS18]
18March 13, 2019 (Wednesday)Graph Based LTL Motion Planning (Dhaval) [KhS18]
--March 18, 2019 (Monday) Mid-Semester Recess
--April 20, 2019 (Wednesday) Mid-Semester Recess
19March 25, 2019 (Monday)Student Presentations 1a and 1b -
20March 27, 2019 (Wednesday)Student Presentations 2a and 2b-
21April 1, 2019 (Monday)Student Presentation 3a and 3b-
22April 3, 2019 (Wednesday)Student Presentations 4a and 4b-
23April 8, 2019 (Monday)Student Presentations 5a and 5b-
24April 10, 2019 (Wednesday)Student Presentations 6a and 6b-
25April 15, 2019 (Monday)Student Presentations 7a, 7b, 7c -
--April 17, 2019 (Wednesday) No Class: Mahavir Jayanti

Schedule for the student presentations

References

[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.