CS698I: Formal Methods for Robotics and Automation

Winter 2016 (December 30, 2015 - April 14, 2016)

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

Lecture Venue: KD103

Instructor: Indranil Saha

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


Topics

  • 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


    • Grading Policy

    Mid-Semester Examination - 20%
    Literature Review and Class Presentation - 20%
    Project - 60%


    Exam Schedule and Deadlines

    Mid-Semester Examination - Feb 15-19, 2016
    Class Presentation - March 28, 2016, March 30, 2016, April 4, 2016
    Project Presentation - April 20, 2016 from 5pm to 7pm, Venue: KD103
    Project Report Submission - April 24, 2016


    Lecture Schedule


    Lecture Date Topic References
    1December 30, 2015Introduction to the course, Modeling Systems[BK08]
    2January 4, 2016Specifying Systems Using Linear Time Properties, Invariant Verification, Safety Properties, Liveness Properties[BK08]
    3January 6, 2016Linear Temporal Logic (LTL), Computation Tree Logic (CTL), Basic Algorithms to Verify LTL and CTL Properties[BK08]
    4January 11, 2016 Discrete-Time Markov Chain (DTMC), Probabilistic Computation Tree Logic (PCTL), Model Checing of DTMC against PCTL Properties[BK08]
    5January 13, 2016Markov Reward Model (MRM), Probabilistic Reward Computation Tree Logic (PRCTL), Markov Decision Process (MDP), Model Checking of MDP against PCTL Properties [BK08]
    6January 18, 2016Fairness, Fairness in CTL, Fairness in LTL[BK08]
    7January 20, 2016Equivalence between LTL and CTL Formulae, Symbolic CTL Model Checking, Binary Decision Diagram (BDD)[BK08], [Bry86]
    8January 25, 2016Synthesis of Reactive Design [PPS06]
    9January 27, 2016SAT and SMT Solvers[NOT06], [BSST09], [dMB08]
    10February 1, 2016Bisimulation Equivalence[BK08]
    11 February 3, 2016 Modeling and Verification of Timed Systems [BK08], [AD94]
    12February 8, 2016Basics of Feedback Control Theory [AM09]
    13February 10, 2016Compositional Temporal Logic Multi-Robot Motion Planning using SMT Solvers [SRK+14]
    --February 15, 2016 Mid-Semester Examination
    --February 17, 2016 Mid-Semester Examination
    14February 22, 2016Basic Search Techniques for Motion Planning[LaV06]
    15February 24, 2016Sampling-Based Motion Planning[LaV06]
    16February 29, 2016Automatic Deployment of Distributed Team of Robots [KB10], [CDSB12]
    17March 2, 2016Incremental Motion Planning for Swarm of Robots [SRK+16]
    18March 7, 2016Multi-Robot Motion Planning for Timed Specification [QBI04]
    19March 9, 2016Reactive Mission and Motion Plan Synthesis from Temporal Logic Specification[KFP09], [WTM12]
    20March 14, 2016Probabilistic Analysis of High-Level Reactive Robot Behavior[JK12]
    21March 16, 2016Revising Motion Planning under Linear Temporal Logic Specifications in Partially Known Workspaces[GHD13]
    --March 21, 2016 Mid-Semester Recess
    --March 23, 2016 Mid-Semester Recess
    22March 28, 2016Motion Planning from Temporal Logic Specifications (Student Presentation) [FGKP09]
    23March 30, 2016Motion Planning from Temporal Logic Specifications (Student Presentation) [BKV10]
    24April 4, 2016Motion Planning from Temporal Logic Specifications (Student Presentation) [USD+13]
    25April 6, 2016Applications beyond Motion Planning: An SMT Approach to Security against Sensor Attackcs, Formal Methods for Semi-Autonomous Driving [SNB+15], [SPN+15], [LSSS14], [SSS15]
    --April 11, 2016No Class: Travel to attend CPSWeek 2016
    --April 13, 2016No Class: Travel to attend CPSWeek 2016


    References

    [AD94] Rajeev Alur, David L. Dill: A Theory of Timed Automata. Theor. Comput. Sci. 126(2): 183-235, 1994.
    [AM09] K. J. Astrom and R. M. Murray. Feedback Systems: An Introduction for Scientists and Engineers. Prince- ton University Press, 2009.
    [Bry86] R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers, 35(8):677-691, 1986.
    [BK08] C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.
    [BKV10] Amit Bhatia, Lydia E. Kavraki, Moshe Y. Vardi: Sampling-based motion planning with temporal goals. ICRA 2010: 2689-2696.
    [BSST09] C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In Armin Biere, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 4, chapter 8. IOS Press, 2009.
    [CDSB12] Yushan Chen, Xu Chu Ding, Alin Stefanescu, Calin Belta: Formal Approach to the Deployment of Distributed Robotic Teams. IEEE Transactions on Robotics 28(1): 158-171 (2012).
    [CGP99] E. M. Clarke, Jr., O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
    [CLH+05] H. Choset, K. M Lynch, S. Hutchinson, G. Kantor, W. Burgard, L. E. Kavraki, and S. Thrun. Principles of Robot Motion: Theory, Algorithms, and Implementations. MIT Press, 2005.
    [dMB08] L. M. de Moura and N. Bjørner. Z3: An efficient smt solver. In TACAS, pages 337-340, 2008.
    [FGKP09] G. E. Fainekos, A. Girard, H. Kress-Gazit, and G. J. Pappas. Temporal logic motion planning for dynamic robots. Automatica, 45(2):343-352, 2009.
    [GHD13] Meng Guo, Karl H. Johansson and Dimos V. Dimarogonas. Revising Motion Planning under Linear Temporal Logic Specifications in Partially Known Workspaces. In ICRA, pages 5025-5032, 2013.
    [JK12] B. Johnson, H. Kress-Gazit: Probabilistic guarantees for high-level robot behavior in the presence of sensor error. Auton. Robots 33(3): 309-321 (2012).
    [KB10] M. Kloetzer and C. Belta. Automatic deployment of distributed teams of robots from temporal logic motion specifications. IEEE Transactions on Robotics, 26(1):48-61, 2010.
    [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.
    [LSSS14] W. Li, D. Sadigh, S. S. Sastry, and S. A. Seshia. Synthesis for human-in-the-loop control systems. In TACAS, pages 470-484, 2014.
    [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.
    [QBI04] M. M. Quottrup, T. Bak, R. Izadi-Zamanabadi: Multi-robot Planning: a Timed Automata Approach. ICRA 2004: 4417-4422.
    [SNB+15] Yasser Shoukry, Pierluigi Nuzzo, Nicola Bezzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Paulo Tabuada: Secure state reconstruction in differentially flat systems under sensor attacks using satisfiability modulo theory solving. CDC 2015: 3804-3809.
    [SPN+15] Yasser Shoukry, Alberto Puggelli, Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, Paulo Tabuada: Sound and complete state estimation for linear dynamical systems under sensor attacks using Satisfiability Modulo Theory solving. ACC 2015: 3818-3823.
    [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.
    [SSS15] Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry: Formal methods for semi-autonomous driving. DAC 2015: 148:1-148:5.
    [USD+13] Alphan Ulusoy, Stephen L. Smith, Xu Chu Ding, Calin Belta, Daniela Rus: Optimality and Robustness in Multi-Robot Path Planning with Temporal Logic Constraints. I. J. Robotic Res. 32(8): 889-911 (2013).
    [WTM12] T. Wongpiromsarn, U. Topcu, R. M. Murray. Receding Horizon Temporal Logic Planning. IEEE Trans. Automat. Contr. 57(11): 2817-2830. 2012.