• Formal Methods
• Model Checking
• Motion planning
• Process Algebra
• RRT*
• Sampling-based Algorithms

The classic motion planning problem - often also referred to as the Piano Mover’s Problem (PM) - has been extensively studied ever since robots and automation started to become a vital part of modern industry and our daily life, being relevant in some other disciplines as well.
In spite of its hard computational complexity, the amount of research on the matter has led to the development of several practically useful approaches, especially during the past decade. In particular we can mention sampling-based algorithms, such as probabilistic roadmaps (PRM) and rapidly exploring random trees (RRT). Informally, the PM problem consists in the task of moving a robot from A to B while avoiding obstacles, where A and B are two configurations or regions of interest in the robot workspace.

However, a large number of robotic applications require to perform more complicated tasks, where the desired plan needs to satisfy some given logical and temporal properties of interest.
For such problems, a major goal is being able to specify the task in a high-level and rigorous formal language and develop provably correct planning algorithms that enable to find and select plans complying with the given mission specification, when any such plan exists.

In the literature many formal languages have been considered to provide rigorous descriptions of motion planning tasks. Among these, we can mention Linear Temporal Logic and Deterministic μ-Calculus. These languages are very powerful and expressive, but for complex cases they might be hardly human-readable - and therefore prone to formulation errors - or require computationally intensive algorithms.
The present work focuses on Process Algebra (PA) as a language to describe a class of mission specifications for optimal motion planning purposes. At the cost of a more limited expressive power, PA is very intuitive and allows efficient model checking algorithms. In spite of its simplicity, though, Process Algebra turns out a powerful tool, prone to non-trivial real world applications.
Application examples are in fact proposed in a future urban mobility-on-demand scenario, and an outline of the implemented solutions is presented with experimental outcomes on a real robotic autonomous golfcar.