RESUMEN
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. In this article, we propose a system model that incorporates a set of uncrewed ground vehicle (UGV) motion constraints, allowing these constraints to be omitted from LTL model checking. This model is used in the LTL synthesizer for path planning, where an LTL property describes only the mission specification. Furthermore, we present a specific parameterization for path planning synthesis using a SPIN. We also offer two SPIN-efficient general LTL formulas for representative UGV missions to reach a DEM partition set, with a specified or unspecified order, respectively. Validation experiments performed on synthetic and real-world DEMs demonstrate the feasibility of the framework for complex mission specifications on DEMs, achieving a significant reduction in computation cost compared to a baseline approach that includes a global LTL property, even when applying appropriate search optimization techniques on both path planners.
RESUMEN
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.g., biased, missing, etc.) that may compromise these operations. Although there exist previous contributions that either address filtering performance or identification of abnormal sensory observations, they do not provide a complete treatment of both problems at once. In this work we present a statistical approach that allows us to study and quantify the impact of abnormal observations from range sensors on the performance of Bayesian filters. For that, we formulate the estimation problem from a generic perspective (abstracting from concrete implementations), analyse the main limitations of common robotics range sensors, and define the factors that potentially affect the filtering performance. Rigorous statistical methods are then applied to a set of simulated experiments devised to reproduce a diversity of situations. The obtained results, which we also validate in a real environment, provide novel and relevant conclusions on the effect of abnormal range observations in these filters.