Automatic synthesis of human motion from temporal logic specifications

Humans and robots are increasingly sharing their workspaces to benefit from the precision, endurance, and strength of machines and the universal capabilities of humans. Instead of performing time-consuming real experiments, computer simulations of humans could help to optimally orchestrate human and robotic tasks - either for setting up new production cells or by optimizing the motion planning of already installed robots. Especially when human-robot coexistence is optimized using machine learning, being able to synthesize a huge number of human motions is indispensable. However, no solution exists that automatically creates a range of human motions from a high-level specification of tasks. We propose a novel method that automatically generates human motions from linear temporal logic specifications and demonstrate our approach by numerical examples.