vTSL - A Formally Verifiable DSL for Specifying Robot Tasks

Abstract

Preprogramming of tasks still plays an important role in complex robotic systems despite the advances in automated planning and symbolic learning. Often, it is desired that end-users implement further tasks to adapt the robotic application to their needs. These user-defined tasks have to meet safety and integrity constraints for protecting the robotic platform and its users. We introduce a verifiable task specification language (vTSL) that enables to automatically prove that a task specification satisfies a set of predefined or task-specific constraints. We illustrate our approach using an example of a self-driving vehicle for intra-logistics and report experiences with two commercial applications.