Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Motion Planning Under Temporal Logic Specifications In Semantically Unknown Environments

Azizollah Taheri, Derya Aksaray

TL;DR

This work tackles motion planning under syntactically co-safe LTL (scLTL) specifications in environments with uncertain semantic labels by modeling uncertainty with a Probabilistically Labeled DMDP (PL-DMDP). An automata-theoretic framework is developed: a total DFA $\mathcal{A}_\phi$ representing the scLTL task is combined with the PL-DMDP into a product automaton $\mathcal{P}$, with edge probabilities $p_p$ encoding label uncertainty. A tailored reward structure and online value iteration drive the synthesis of a policy $\pi_p^*$ that seeks to reach accepting states while avoiding trash states, updating beliefs as true labels are revealed and re-planning when necessary. The approach is validated through case studies on gridworlds and benchmark analyses showing favorable trajectory lengths and runtime performance against prior offline methods, with demonstrated resilience to incorrect initial beliefs and scalable online replanning. The results have practical implications for robust autonomous navigation in partially known environments, offering a principled path to integrate semantic uncertainty into real-time planning and control.

Abstract

This paper addresses a motion planning problem to achieve spatio-temporal-logical tasks, expressed by syntactically co-safe linear temporal logic specifications (scLTL\next), in uncertain environments. Here, the uncertainty is modeled as some probabilistic knowledge on the semantic labels of the environment. For example, the task is "first go to region 1, then go to region 2"; however, the exact locations of regions 1 and 2 are not known a priori, instead a probabilistic belief is available. We propose a novel automata-theoretic approach, where a special product automaton is constructed to capture the uncertainty related to semantic labels, and a reward function is designed for each edge of this product automaton. The proposed algorithm utilizes value iteration for online replanning. We show some theoretical results and present some simulations/experiments to demonstrate the efficacy of the proposed approach.

Motion Planning Under Temporal Logic Specifications In Semantically Unknown Environments

TL;DR

This work tackles motion planning under syntactically co-safe LTL (scLTL) specifications in environments with uncertain semantic labels by modeling uncertainty with a Probabilistically Labeled DMDP (PL-DMDP). An automata-theoretic framework is developed: a total DFA representing the scLTL task is combined with the PL-DMDP into a product automaton , with edge probabilities encoding label uncertainty. A tailored reward structure and online value iteration drive the synthesis of a policy that seeks to reach accepting states while avoiding trash states, updating beliefs as true labels are revealed and re-planning when necessary. The approach is validated through case studies on gridworlds and benchmark analyses showing favorable trajectory lengths and runtime performance against prior offline methods, with demonstrated resilience to incorrect initial beliefs and scalable online replanning. The results have practical implications for robust autonomous navigation in partially known environments, offering a principled path to integrate semantic uncertainty into real-time planning and control.

Abstract

This paper addresses a motion planning problem to achieve spatio-temporal-logical tasks, expressed by syntactically co-safe linear temporal logic specifications (scLTL\next), in uncertain environments. Here, the uncertainty is modeled as some probabilistic knowledge on the semantic labels of the environment. For example, the task is "first go to region 1, then go to region 2"; however, the exact locations of regions 1 and 2 are not known a priori, instead a probabilistic belief is available. We propose a novel automata-theoretic approach, where a special product automaton is constructed to capture the uncertainty related to semantic labels, and a reward function is designed for each edge of this product automaton. The proposed algorithm utilizes value iteration for online replanning. We show some theoretical results and present some simulations/experiments to demonstrate the efficacy of the proposed approach.

Paper Structure

This paper contains 20 sections, 6 theorems, 13 equations, 6 figures, 3 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Notation and Graph Theory
  5. Probabilistically Labeled DMDP
  6. Temporal logic
  7. Problem Formulation
  8. Solution Approach
  9. Product Automaton
  10. Reward Design And Value Iteration
  11. Main Algorithm
  12. $\mathcal{X} = \emptyset$
  13. $\mathcal{X} \neq \emptyset$
  14. Case Studies
  15. Ordering Reachability with Avoidance
  16. ...and 5 more sections

Key Result

Lemma 1

A policy $\pi_p$ is a non-zero probability satisfying policy if and only if it satisfies the condition $U^{\pi_p}(s_p) > \frac{-\beta}{1 - \gamma}$ for all $s_p \in \mathcal{S}_p \setminus (\mathcal{F}_a \cup \mathcal{F}_t)$.

Figures (6)

  • Figure 1: (a) A drone in an environment aims to visit Region 1 first, and then Region 2, without prior knowledge of their exact locations. (b) The drone's initial belief about the possible locations of regions 1 and 2. The values represent independent probabilities for the cells, indicating the likelihood of a cell having that label (or no label otherwise).
  • Figure 2: An illustration of PL-DMDP $\mathcal{M}_1 = (X, \Sigma, \delta, O, L, l_{true}, p_L, c)$ where $X=\{x_0, x_1, x_2, x_3\}$, $\Sigma=\{Up,Right,Down,Left,Stay\}$, and $O=\{r_1,r_2\}$. Some examples of $\delta$, $L$, and $p_L$ are $\delta(x_0, Right)=x_1$, $L(x_0) = \{{\{r_1\},\{r_2\},\{r_1,r_2\},\{\}}\}$, $p_L(x_1, \{r_1\}) = 0.2$, respectively.
  • Figure 3: A portion of the product automaton showing only the outgoing edges from $(x_0, s_0)$ under action $Right$, along with their associated probabilities and rewards.
  • Figure 4: Outline of the proposed framework.
  • Figure 5: The illustrations of (a) the planned trajectory in red based on the initial belief, (b,c,d,e) the re-planned trajectories in red based on the current belief and the realized trajectory in black, (f) the final trajectory accomplishing the mission.
  • ...and 1 more figures

Theorems & Definitions (19)

  • Definition 1: PL-DMDP
  • Definition 2: $\text{scLTL}_{\setminus{\emph{next}}}$
  • Definition 3: DFA
  • Definition 4: Total DFA
  • Definition 5: Product automaton
  • Definition 6: Uncertain States
  • Definition 7: Non-zero probability satisfying policy
  • Lemma 1
  • proof
  • Corollary 1
  • ...and 9 more