Temporal logic control for an autonomous quadrotor in a nondeterministic environment

We present an experimental setup for automatic deployment of a quadrotor in an environment with known topology and nondeterministically changing properties. The missions are specified as rich, temporal logic statements about the satisfaction of the properties. The main objective is to be able to synthesize, test, and evaluate control policies for complex aerial missions. Our testbed consists of quadrotors, a motion capture system that provides precise and continuous position information of the quadrotor, projectors that can emulate dynamically changing environments, physical obstacles, and computers that control the quadrotor, the motion capture system, and the projectors. Our computational approach is hierarchical. At the bottom level, we partition the environment and construct an abstraction in the form of a finite transition system such that the quadrotor can execute its transitions by using low level feedback controllers. At the top level, we draw inspiration from LTL model checking and use a value iteration algorithm to determine an optimal control policy that guarantees the satisfaction of the specification under nondeterministically changing properties. We illustrate the approach for the particular case of a surveillance mission in a city-like environment.