Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Optimization-based Task and Motion Planning under Signal Temporal Logic Specifications using Logic Network Flow

Xuan Lin, Jiming Ren, Samuel Coogan, Ye Zhao

Abstract

This paper proposes an optimization-based task and motion planning framework, named "Logic Network Flow", to integrate signal temporal logic (STL) specifications into efficient mixed-binary linear programmings. In this framework, temporal predicates are encoded as polyhedron constraints on each edge of the network flow, instead of as constraints between the nodes as in the traditional Logic Tree formulation. Synthesized with Dynamic Network Flows, Logic Network Flows render a tighter convex relaxation compared to Logic Trees derived from these STL specifications. Our formulation is evaluated on several multi-robot motion planning case studies. Empirical results demonstrate that our formulation outperforms Logic Tree formulation in terms of computation time for several planning problems. As the problem size scales up, our method still discovers better lower and upper bounds by exploring fewer number of nodes during the branch-and-bound process, although this comes at the cost of increased computational load for each node when exploring branches.

Optimization-based Task and Motion Planning under Signal Temporal Logic Specifications using Logic Network Flow

Abstract

This paper proposes an optimization-based task and motion planning framework, named "Logic Network Flow", to integrate signal temporal logic (STL) specifications into efficient mixed-binary linear programmings. In this framework, temporal predicates are encoded as polyhedron constraints on each edge of the network flow, instead of as constraints between the nodes as in the traditional Logic Tree formulation. Synthesized with Dynamic Network Flows, Logic Network Flows render a tighter convex relaxation compared to Logic Trees derived from these STL specifications. Our formulation is evaluated on several multi-robot motion planning case studies. Empirical results demonstrate that our formulation outperforms Logic Tree formulation in terms of computation time for several planning problems. As the problem size scales up, our method still discovers better lower and upper bounds by exploring fewer number of nodes during the branch-and-bound process, although this comes at the cost of increased computational load for each node when exploring branches.
Paper Structure (14 sections, 12 equations, 7 figures, 2 tables, 1 algorithm)

This paper contains 14 sections, 12 equations, 7 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Temporal Logic Preliminaries
  4. Logic Tree
  5. Branch and Bound
  6. Proposed Method
  7. Logic Network Flow
  8. Optimization Formulation
  9. Incorporating Dynamics as Dynamic Network Flow
  10. Complete Formulation
  11. Experiments
  12. Multi-agent Coordination Tasks
  13. Planning Robot Motions to Search over a Map
  14. Conclusion

Figures (7)

  • Figure 1: An example of a Logic Tree (Left) and a Logic Network Flow (Right) for the specification $\varphi=((z^{\pi_{1}} \wedge z^{\pi_{2}}) \vee (z^{\pi_{3}} \wedge z^{\pi_{4}})) \vee ((z^{\pi_{5}} \wedge z^{\pi_{6}}) \wedge (z^{\pi_{7}} \vee z^{\pi_{8}})) \vee (z^{\pi_{9}} \vee z^{\pi_{10}} \vee z^{\pi_{11}})$.
  • Figure 2: The Logic Tree for $\Diamond_{[0,2]}(\square_{[0,1]} \pi)$, given in Example \ref{['exp: example1']}.
  • Figure 3: An illustration of the strategy to translate conjunction and disjunction combination types from LTs to LNFs in Algorithm \ref{['Algorithm:build_node']}.
  • Figure 4: An example of an LT transformed into an LNF by applying Algorithm \ref{['Algorithm:build_node']}. Each edge in the LNF possesses a binary variable $y_i$ and a vector variable $\boldsymbol{\omega}_i$, given in Example \ref{['fig:example3']}.
  • Figure 5: A discretized Georgia Tech map, including 6 sites of interest shown as red dots and 7 interval knots shown as black dots, is used in Sec. \ref{['subsec:mutliagent']}. It takes each robot $dT$ to travel along each blue line segment divided by black dots in the graph.
  • ...and 2 more figures

Theorems & Definitions (4)

  • Definition 1
  • Example 1
  • Definition 2
  • Example 2