In manufacturing, the current trend-shift from mass-production to mass-personalization is enabled, among others, by the emerging field of human-robot collaboration (HRC), in which humans collaborate or work in proximity with robots. In HRC scenarios, robots need to exert a desired behaviour that maximizes utility without sacrificing safety and responsiveness. To maximize safety and utility in static environments, state-of-the-art offline motion-planners use computationally-heavy algorithms for approximating the collision-free robot reachability and accordingly generate (sub-)optimal robot trajectories. To enable real-time responsiveness, we propose an integrated global planner to generate sub-optimal trajectories. It relies on a closed-loop reactive controller for executing the global plan while ensuring safety with practical assumptions about the environment. We evaluate GLIR in simulation. In our experiments, our global planner operates at 25 Hz and the local planner at 100 Hz, enabling their execution in dynamic environments. In all experiments on static scenes with static and dynamic goals, GLIR keeps a safety distance from obstacles. We showcase some simulation experiments and a real-world demonstration in the video available at https://mohamedgalil.github.io/glir/.

In this paper, we propose a novel representation and verification technique for software components in a robotic system using a linear logic theorem prover. Linear logic includes consumable resources together with persistent resources, enabling representing and reasoning of robotic domains. We demonstrate model representation and verification of formal specifications through Robot Operating System (ROS) components. The system model can be either statically extracted by HAROS (a ROS based static analysis framework) or dynamically extracted once all system components are running. After ten years of its first release, ROS has become one of the most popular middlewares among robotic programming frameworks. Even though ROS is very popular among robotic developers, we believe that a framework for easily representing and verifying robotic systems is missing. This paper introduces a new technique for formally representing and verifying robotic systems using a linear logic theorem prover and finally presents a number of illustrations of model representation and safety property checking both statically and dynamically for the robot Kobuki.

Reacting to unexpected conditions and recovering from errors is crucial for robots to perform their missions continuously in dynamic environments. This paper introduces a novel framework aiming to handle errors impairing the quality of robot services concerning on-line management of error recovery. The framework is a combination of an execution generation tool, a learning module, and a recovery pipeline for error detection, diagnosis, and recovery in robotic systems. The execution generation tool generates control flow instructions and parameter files, then extracts necessary skills from the skill library based on application descriptions or recovery solution recipes. In the learning module, a Bayesian Network (BN) decision model is interactively and continually trained, incorporating application information structured according to the Failure Mode and Effects Analysis (FMEA) method. The recovery pipeline implements a decision model inferring the cause of an error and choosing recovery solutions. We will provide an experimental evaluation of our framework on a pick-and-place application performed by a robot arm in the physical world.

In this paper, we introduce a novel logic language and theorem prover for robotic task planning. Our language, which we call Linear Planning Logic (LPL), is a fragment of linear logic whose resource-conscious semantics are well suited for reasoning with dynamic state, while its structure admits efficient theorem provers for automatic plan construction. LPL can be considered as an extension of Linear Hereditary Harrop Formulas (LHHF), whose careful design allows the minimization of nondeterminism in proof search, providing a sufficient basis for the design of linear logic programming languages such as Lolli. Our new language extends on the expressivity of LHHF, while keeping the resulting nondeterminism in proof search to a minimum for efficiency. This paper introduces the LPL language, presents the main ideas behind our theorem prover on a smaller fragment of this language and finally provides an experimental illustration of its operation on the problem of task planning for the hexapod robot RHex.