SPIN-Based Linear Temporal Logic Path Planning for Ground Vehicle Missions with Motion Constraints on Digital Elevation Models.

Linear temporal logic (LTL) formalism can ensure the correctness of mobile robot planning through concise, readable, and verifiable mission specifications. For uneven terrain, planning must consider motion constraints related to asymmetric slope traversability and maneuverability. However, even though model checker tools like the open-source Simple Promela Interpreter (SPIN) include search optimization techniques to address the state explosion problem, defining a global LTL property that encompasses both mission specifications and motion constraints on digital elevation models (DEMs) can lead to complex models and high computation times.

Statistical Study of the Performance of Recursive Bayesian Filters with Abnormal Observations from Range Sensors.

Range sensors are currently present in countless applications related to perception of the environment. In mobile robots, these devices constitute a key part of the sensory apparatus and enable essential operations, that are often addressed by applying methods grounded on probabilistic frameworks such as Bayesian filters. Unfortunately, modern mobile robots have to navigate within challenging environments from the perspective of their sensory devices, getting abnormal observations (e.