Motion Planning for Automata-based Objectives using Efficient Gradient-based Methods

TL;DR

This paper introduces a gradient-based optimization approach for automata-based objectives in motion planning, enabling scalable and efficient handling of complex temporal tasks without extensive trajectory storage.

Contribution

It presents a novel method that encodes symbolic automata as matrix operators suitable for automatic differentiation, improving scalability over traditional STL-based approaches.

Findings

Enables efficient gradient-based optimization for automata objectives.

Reduces memory requirements by avoiding storage of long system trajectories.

Demonstrates improved scalability for complex temporal tasks.

Abstract

In recent years, there has been increasing interest in using formal methods-based techniques to safely achieve temporal tasks, such as timed sequence of goals, or patrolling objectives. Such tasks are often expressed in real-time logics such as Signal Temporal Logic (STL), whereby, the logical specification is encoded into an optimization problem. Such approaches usually involve optimizing over the quantitative semantics, or robustness degree, of the logic over bounded horizons: the semantics can be encoded as mixed-integer linear constraints or into smooth approximations of the robustness degree. A major limitation of this approach is that it faces scalability challenges with respect to temporal complexity: for example, encoding long-term tasks requires storing the entire history of the system. In this paper, we present a quantitative generalization of such tasks in the form of symbolic automata objectives. Specifically, we show that symbolic automata can be expressed as matrix operators that lend themselves to automatic differentiation, allowing for the use of off-the-shelf gradient-based optimizers. We show how this helps solve the need to store arbitrarily long system trajectories, while efficiently leveraging the task structure encoded in the automaton.