Planning and Specification Problems for Multi-Robot Systems, Powered by Formal Methods

Robotic systems are entering the stage. Enabled by advances in both hardware components and software techniques, robots are increasingly able to operate outside of factories, assist humans, and work alongside them. The limiting factor of robots’ expansion remains the programming of robotic systems. Due to the many diverse skills necessary to build a multi-robot system, only the biggest organizations are able to innovate in the space of services provided by robots. To make developing new robotic services easier, in this dissertation I propose a program- ming model in which users (programmers) give a declarative specification of what needs to be accomplished, and then a backend system makes sure that the specification is safely and reliably executed. I present Antlab, one such backend system. Antlab accepts Linear Temporal Logic (LTL) specifications from multiple users and executes them using a set of robots of different capabilities. Building on the experience acquired implementing Antlab, I identify problems arising from the proposed programming model. These problems fall into two broad categories, specification and planning. In the category of specification problems, I solve the problem of inferring an LTL formula from sets of positive and negative example traces, as well as from a set of positive examples only. Building on top of these solutions, I develop a method to help users transfer their intent into a formal specification. The approach taken in this dissertation is combining the intent signals from a single demonstration and a natural language description given by a user. A set of candidate specifications is inferred by encoding the problem as a satisfiability problem for propositional logic. This set is narrowed down to a single specification through interaction with the user; the user approves or declines generated simulations of the robot’s behavior in different situations. In the category of planning problems, I first solve the problem of planning for robots that are currently executing their tasks. In such a situation, it is unclear what to take as the initial state for planning. I solve the problem by considering multiple, speculative initial states. The paths from those states are explored based on a quality function that repeatedly estimates the planning time. The second problem is a problem of reinforcement learning when the reward function is non-Markovian. The proposed solution consists of iteratively learning an automaton representing the reward function and using it to guide the exploration