Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Temporal-Logic-Aware Frontier-Based Exploration

Azizollah Taheri, Derya Aksaray

TL;DR

This paper introduces a new type of automaton state, referred to as commit states, that capture intermediate task progress resulting from actions whose consequences are irreversible, and proposes a sound and complete frontier-based exploration algorithm that strategically guides the robot to make progress toward the task while preserving all possible ways of satisfying it.

Abstract

This paper addresses the problem of temporal logic motion planning for an autonomous robot operating in an unknown environment. The objective is to enable the robot to satisfy a syntactically co-safe Linear Temporal Logic (scLTL) specification when the exact locations of the desired labels are not known a priori. We introduce a new type of automaton state, referred to as commit states. These states capture intermediate task progress resulting from actions whose consequences are irreversible. In other words, certain future paths to satisfaction become not feasible after taking those actions that lead to the commit states. By leveraging commit states, we propose a sound and complete frontier-based exploration algorithm that strategically guides the robot to make progress toward the task while preserving all possible ways of satisfying it. The efficacy of the proposed method is validated through simulations.

Temporal-Logic-Aware Frontier-Based Exploration

TL;DR

This paper introduces a new type of automaton state, referred to as commit states, that capture intermediate task progress resulting from actions whose consequences are irreversible, and proposes a sound and complete frontier-based exploration algorithm that strategically guides the robot to make progress toward the task while preserving all possible ways of satisfying it.

Abstract

This paper addresses the problem of temporal logic motion planning for an autonomous robot operating in an unknown environment. The objective is to enable the robot to satisfy a syntactically co-safe Linear Temporal Logic (scLTL) specification when the exact locations of the desired labels are not known a priori. We introduce a new type of automaton state, referred to as commit states. These states capture intermediate task progress resulting from actions whose consequences are irreversible. In other words, certain future paths to satisfaction become not feasible after taking those actions that lead to the commit states. By leveraging commit states, we propose a sound and complete frontier-based exploration algorithm that strategically guides the robot to make progress toward the task while preserving all possible ways of satisfying it. The efficacy of the proposed method is validated through simulations.
Paper Structure (18 sections, 1 theorem, 5 equations, 7 figures, 1 table, 1 algorithm)

This paper contains 18 sections, 1 theorem, 5 equations, 7 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Transition System
  5. Temporal logic
  6. Graph Theory
  7. Problem Formulation
  8. Solution Approach
  9. Offline
  10. Online
  11. TL-Aware Frontier-Based Exploration
  12. Information gain
  13. Task progress metric
  14. Algorithm
  15. Case Studies
  16. ...and 3 more sections

Key Result

Theorem 1

Let Assumptions sensor and entering_commit hold. Then, Alg. alg is sound and complete.

Figures (7)

  • Figure 1: The DFA $\mathcal{A}$ corresponding to formula $\phi_0$.
  • Figure 2: A portion of $\bar{\mathcal{A}}$ showing all states reachable from the initial state $\bar{s}_0 = (3,1)$.
  • Figure 3: A portion of $\bar{\mathcal{A}}$ showing all states reachable from the initial state $\bar{s}'_0 = (3,2)$.
  • Figure 4: Summary of the proposed method.
  • Figure 5: Snapshots from a video, starting at (a) and ending at (e), illustrating the robot executing our algorithm to satisfy the task $\phi_1$. The robot’s starting position is marked by a red circle in the top-left corner, while the lower-level region, person, and safe exit are represented by yellow, green, and blue squares, respectively. The robot’s traversed trajectory is shown by black arrows.
  • ...and 2 more figures

Theorems & Definitions (12)

  • Definition 1: Weighted Deterministic Transition System
  • Definition 2: $\text{scLTL}_{\setminus{\emph{next}}}$
  • Definition 3: DFA
  • Definition 4: Total DFA
  • Definition 5: DFA with altered initial state
  • Definition 6: Commit state
  • Example
  • Definition 7: Product Automaton (DFA-DFA)
  • Example
  • Definition 8: Product Automaton (TS-DFA)
  • ...and 2 more