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

TL;DR

It is shown 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, and how this helps solve the need to store arbitrarily long system trajectories, while efficiently leveraging the task structure encoded in the automaton.

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.

Figures (3)

• Figure 1: Example of a symbolic automaton describing the specification "move to region $\mathcal{R}_{\text{red}}$, then region $\mathcal{R}_{\text{green}}$, and then to region $\mathcal{R}_{\text{orange}}$ in order while always avoiding region $\mathcal{R}_{\text{blue}}$. " An accepting run in the automaton is a sequence of states $\bm{x} \in \Sigma^*$ that moves the automaton location from the initial location $q_0$ to the accepting location $q_3$.
• Figure 2: An example trajectory in a 2D workspace that satisfies the specification in \ref{['fig:sa-example']}. Here, the state $x$ is a vector in $\mathbb{R}^2$, and the trajectory starts at a point $(-1, -1)$ and completes the specified task.
• Figure 3: Example of a trajectory satisfying $\varphi_1$ and $\varphi_2$. The left-side trajectory was produced by the $(\min,\max)$ automaton in a single integrator dynamics model, while the second one was produced by the $(\max, +)$ automaton for unicycle model.

Theorems & Definitions (12)

• Remark
• Definition 1: Symbolic Automata dantoni2017power
• Remark
• Example 1
• Definition 2: Semiring mohri2002semiring
• Definition 3: Symbolic Weighted Automata droste2009handbookdantoni2017powerjaksic2018algebraic
• Remark
• Example 2: Weights of a path
• Remark
• Definition 4: Generalized Weights