SURF 2012: Formal verification of patching algorithms for SLAM tasks

From Murray Wiki
Jump to navigationJump to search

2012 SURF project description

  • Mentor: Richard Murray
  • Co-mentor: Pavithra Prabhakar, Scott Livingston

After decades of progress in fundamental aspects of robotics, a major paradigm in modern research is so-called task-level planning [1,2]. In addition to generating a plan to move from a point~A to a point~B, such research is directed at more sophisticated behaviors such as surveillance, response to unpredictable flags and appropriate environment interaction. In this project we will explore incremental plan generation, or patching, wherein a plan to perform a task is improved online as new sensor data becomes available. In particular, we consider the scenario of simultaneous localization and mapping (SLAM) [5]. While a formal specification is given at initialization, its realization must be nominally synthesized and patched online as a map of the environment is built, subject to reasonable assumptions on uncertainty. We seek to develop methods to ensure correctness throughout SLAM.

Project goals

  • extend an existing --or design and implement a new-- patching algorithm for simultaneous localization and mapping;
  • demonstrate in simulation (e.g., Stage or Gazebo);
  • experiment on mobile robots (e.g., Landroids or Pioneers), both in controlled lab setup and on an office building floor.

Pre-requisites

  • Comfortable working in GNU/Linux (or BSD, etc.).
  • Good knowledge of Python, C, or C++ programming languages.
  • Some experience with experimental robotics is desired but not necessary.

References

  1. C. Belta, A. Bicchi, M. Egerstedt, E. Frazzoli, E. Klavins and G. J. Pappas, Symbolic Planning and Control of Robot Motion: Finding th Missing Pieces of Current Methods and Ideas, IEEE Robotics & Automation Magazine, pp.~61--70, Mar~2007.
  2. H. Kress-Gazit, T. Wongpiromsarn, U. Topcu, Correct, reactive robot control from abstraction and temporal logic specifications, IEEE Robotics & Automation Magazine, Sep 2011.
  3. S. C. Livingston, R. M. Murray, J. W. Burdick, Backtracking temporal logic synthesis for uncertain environments, Submitted, Sep~2011.
  4. B. Johnson, H Kress-Gazit, Probabilistic analysis of correctness of high-level robot behavior with sensor error, Proc. RSS, 2011.
  5. S. Thrun, W. Burgard, D. Fox, Probabilistic Robotics, MIT~Press, 2005.
Retrieved from "https://murray.cds.caltech.edu/index.php?title=SURF_2012:_Formal_verification_of_patching_algorithms_for_SLAM_tasks&oldid=13383"