Tag Archives: Useful For Teaching

A theoretical framework based on hybrid models and logical verification to prove the guarantees for obstacle avoidance in mobile robot navigation

Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer, Formal verification of obstacle avoidance and navigation of ground robots, The International Journal of Robotics Research Vol 36, Issue 12, pp. 1312 – 1340, DOI: 0.1177/0278364917733549.

This article answers fundamental safety questions for ground robot navigation: under which circumstances does which control decision make a ground robot safely avoid obstacles? Unsurprisingly, the answer depends on the exact formulation of the safety objective, as well as the physical capabilities and limitations of the robot and the obstacles. Because uncertainties about the exact future behavior of a robot’s environment make this a challenging problem, we formally verify corresponding controllers and provide rigorous safety proofs justifying why the robots can never collide with the obstacle in the respective physical model. To account for ground robots in which different physical phenomena are important, we analyze a series of increasingly strong properties of controllers for increasingly rich dynamics and identify the impact that the additional model parameters have on the required safety margins. We analyze and formally verify: (i) static safety, which ensures that no collisions can happen with stationary obstacles; (ii) passive safety, which ensures that no collisions can happen with stationary or moving obstacles while the robot moves; (iii) the stronger passive-friendly safety, in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well; and (iv) passive orientation safety, which allows for imperfect sensor coverage of the robot, i.e., the robot is aware that not everything in its environment will be visible. We formally prove that safety can be guaranteed despite sensor uncertainty and actuator perturbation. We complement these provably correct safety properties with liveness properties: we prove that provably safe motion is flexible enough to let the robot navigate waypoints and pass intersections. To account for the mixed influence of discrete control decisions and the continuous physical motion of the ground robot, we develop corresponding hybrid system models and use differential dynamic logic theorem-proving techniques to formally verify their correctness. Since these models identify a broad range of conditions under which control decisions are provably safe, our results apply to any control algorithm for ground robots with the same dynamics. As a demonstration, we also synthesize provably correct runtime monitor conditions that check the compliance of any control algorithm with the verified control decisions.

An open-source implementation of visual SLAM with a very nice related-work section

R. Mur-Artal and J. D. Tardós, ORB-SLAM2: An Open-Source SLAM System for Monocular, Stereo, and RGB-D Cameras, IEEE Transactions on Robotics, vol. 33, no. 5, pp. 1255-1262, DOI: 10.1109/TRO.2017.2705103.

We present ORB-SLAM2, a complete simultaneous localization and mapping (SLAM) system for monocular, stereo and RGB-D cameras, including map reuse, loop closing, and relocalization capabilities. The system works in real time on standard central processing units in a wide variety of environments from small hand-held indoors sequences, to drones flying in industrial environments and cars driving around a city. Our back-end, based on bundle adjustment with monocular and stereo observations, allows for accurate trajectory estimation with metric scale. Our system includes a lightweight localization mode that leverages visual odometry tracks for unmapped regions and matches with map points that allow for zero-drift localization. The evaluation on 29 popular public sequences shows that our method achieves state-of-the-art accuracy, being in most cases the most accurate SLAM solution. We publish the source code, not only for the benefit of the SLAM community, but with the aim of being an out-of-the-box SLAM solution for researchers in other fields.

Interesting implementation of visual graph SLAM in C++ for educational purposes

Dominik Schlegel, Mirco Colosi, Giorgio Grisetti, ProSLAM: Graph SLAM from a Programmer’s Perspective/strong>, arXiv:1709.04377.

In this paper we present ProSLAM, a lightweight stereo visual SLAM system designed with simplicity in mind. Our work stems from the experience gathered by the authors while teaching SLAM to students and aims at providing a highly modular system that can be easily implemented and understood. Rather than focusing on the well known mathematical aspects of Stereo Visual SLAM, in this work we highlight the data structures and the algorithmic aspects that one needs to tackle during the design of such a system. We implemented ProSLAM using the C++ programming language in combination with a minimal set of well known used external libraries. In addition to an open source implementation, we provide several code snippets that address the core aspects of our approach directly in this paper. The results of a thorough validation performed on standard benchmark datasets show that our approach achieves accuracy comparable to state of the art methods, while requiring substantially less computational resources.

A nice summary of motion planning

J. J. M. Lunenburg, S. A. M. Coenen, G. J. L. Naus, M. J. G. van de Molengraft and M. Steinbuch, “Motion Planning for Mobile Robots: A Method for the Selection of a Combination of Motion-Planning Algorithms,” in IEEE Robotics & Automation Magazine, vol. 23, no. 4, pp. 107-117, Dec. 2016. DOI: 10.1109/MRA.2015.2510798.

A motion planner for mobile robots is commonly built out of a number of algorithms that solve the two steps of motion planning: 1) representing the robot and its environment and 2) searching a path through the represented environment. However, the available literature on motion planning lacks a generic methodology to arrive at a combination of representations and search algorithm classes for a practical application. This article presents a method to select appropriate algorithm classes that solve both the steps of motion planning and to select a suitable approach to combine those algorithm classes. The method is verified by comparing its outcome with three different motion planners that have been successfully applied on robots in practice.

An excellent survey of metrical SLAM (and of map representations and other issues related to SLAM) as of 2016

C. Cadena et al., “Past, Present, and Future of Simultaneous Localization and Mapping: Toward the Robust-Perception Age,” in IEEE Transactions on Robotics, vol. 32, no. 6, pp. 1309-1332, Dec. 2016. DOI: 10.1109/TRO.2016.2624754.

Simultaneous localization and mapping (SLAM) consists in the concurrent construction of a model of the environment (the map), and the estimation of the state of the robot moving within it. The SLAM community has made astonishing progress over the last 30 years, enabling large-scale real-world applications and witnessing a steady transition of this technology to industry. We survey the current state of SLAM and consider future directions. We start by presenting what is now the de-facto standard formulation for SLAM. We then review related work, covering a broad set of topics including robustness and scalability in long-term mapping, metric and semantic representations for mapping, theoretical performance guarantees, active SLAM and exploration, and other new frontiers. This paper simultaneously serves as a position paper and tutorial to those who are users of SLAM. By looking at the published research with a critical eye, we delineate open challenges and new research issues, that still deserve careful scientific investigation. The paper also contains the authors’ take on two questions that often animate discussions during robotics conferences: Do robots need SLAM? and Is SLAM solved?

A novel particle filter algorithm with an adaptive number of particles, and a curious and interesting table I about the pros and cons of different sensors

T. de J. Mateo Sanguino and F. Ponce Gómez, “Toward Simple Strategy for Optimal Tracking and Localization of Robots With Adaptive Particle Filtering,” in IEEE/ASME Transactions on Mechatronics, vol. 21, no. 6, pp. 2793-2804, Dec. 2016.DOI: 10.1109/TMECH.2016.2531629.

The ability of robotic systems to autonomously understand and/or navigate in uncertain environments is critically dependent on fairly accurate strategies, which are not always optimally achieved due to effectiveness, computational cost, and parameter settings. In this paper, we propose a novel and simple adaptive strategy to increase the efficiency and drastically reduce the computational effort in particle filters (PFs). The purpose of the adaptive approach (dispersion-based adaptive particle filter – DAPF) is to provide higher number of particles during the initial searching state (when the localization presents greater uncertainty) and fewer particles during the subsequent state (when the localization exhibits less uncertainty). With the aim of studying the dynamical PF behavior regarding others and putting the proposed algorithm into practice, we designed a methodology based on different target applications and a Kinect sensor. The various experiments conducted for both color tracking and mobile robot localization problems served to demonstrate that the DAPF algorithm can be further generalized. As a result, the DAPF approach significantly improved the computational performance over two well-known filtering strategies: 1) the classical PF with fixed particle set sizes, and 2) the adaptive technique named Kullback-Leiber distance.

Survey and taxonomy of path planning algorithms

Thi Thoa Mac, Cosmin Copot, Duc Trung Tran, Robin De Keyser, Heuristic approaches in robot path planning: A survey, Robotics and Autonomous Systems, Volume 86, 2016, Pages 13-28, ISSN 0921-8890, DOI: 10.1016/j.robot.2016.08.001.

Autonomous navigation of a robot is a promising research domain due to its extensive applications. The navigation consists of four essential requirements known as perception, localization, cognition and path planning, and motion control in which path planning is the most important and interesting part. The proposed path planning techniques are classified into two main categories: classical methods and heuristic methods. The classical methods consist of cell decomposition, potential field method, subgoal network and road map. The approaches are simple; however, they commonly consume expensive computation and may possibly fail when the robot confronts with uncertainty. This survey concentrates on heuristic-based algorithms in robot path planning which are comprised of neural network, fuzzy logic, nature-inspired algorithms and hybrid algorithms. In addition, potential field method is also considered due to the good results. The strengths and drawbacks of each algorithm are discussed and future outline is provided.

Combining efficiently symbolic planning with geometric planning

Fabien Lagriffoul, Benjamin Andres (2016), Combining task and motion planning: A culprit detection problem , The International Journal of Robotics Research, Vol 35, Issue 8, pp. 890 – 927, DOI: 10.1177/0278364915619022.

Solving problems combining task and motion planning requires searching across a symbolic search space and a geometric search space. Because of the semantic gap between symbolic and geometric representations, symbolic sequences of actions are not guaranteed to be geometrically feasible. This compels us to search in the combined search space, in which frequent backtracks between symbolic and geometric levels make the search inefficient. We address this problem by guiding symbolic search with rich information extracted from the geometric level through culprit detection mechanisms.

A gentle introduction to Box-Particle Filters

A. Gning, B. Ristic, L. Mihaylova and F. Abdallah, An Introduction to Box Particle Filtering [Lecture Notes], in IEEE Signal Processing Magazine, vol. 30, no. 4, pp. 166-171, July 2013. DOI: 10.1109/MSP.2013.225460.

Resulting from the synergy between the sequential Monte Carlo (SMC) method [1] and interval analysis [2], box particle filtering is an approach that has recently emerged [3] and is aimed at solving a general class of nonlinear filtering problems. This approach is particularly appealing in practical situations involving imprecise stochastic measurements that result in very broad posterior densities. It relies on the concept of a box particle that occupies a small and controllable rectangular region having a nonzero volume in the state space. Key advantages of the box particle filter (box-PF) against the standard particle filter (PF) are its reduced computational complexity and its suitability for distributed filtering. Indeed, in some applications where the sampling importance resampling (SIR) PF may require thousands of particles to achieve accurate and reliable performance, the box-PF can reach the same level of accuracy with just a few dozen box particles. Recent developments [4] also show that a box-PF can be interpreted as a Bayes? filter approximation allowing the application of box-PF to challenging target tracking problems [5].

Real-time trajectory generation for omnidirectional robots, and a good set of basic bibliographical references

Tamás Kalmár-Nagy, Real-time trajectory generation for omni-directional vehicles by constrained dynamic inversion, Mechatronics, Volume 35, May 2016, Pages 44-53, ISSN 0957-4158, DOI: 10.1016/j.mechatronics.2015.12.004.

This paper presents a computationally efficient algorithm for real-time trajectory generation for omni-directional vehicles. The algorithm uses a dynamic inversion based approach that incorporates vehicle dynamics, actuator saturation and bounded acceleration. The algorithm is compared with other trajectory generation algorithms for omni-directional vehicles. The method yields good quality trajectories and is implementable in real-time. Numerical and hardware tests are presented.