Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Robust MITL planning under uncertain navigation times

Alexis Linard, Anna Gautier, Daniel Duberg, Jana Tumova

TL;DR

The paper tackles robust task planning for robots under time-varying navigation durations by optimizing MITL temporal robustness. It first develops a MILP encoding for a $VWTS$ to handle deterministic, time-dependent travel times, and then extends the framework to $MDP$s to accommodate stochastic delays, including a receding-horizon planner that preserves robustness guarantees via worst-case lookahead. A two-stage MILP with history augmentation enables synthesis under uncertainty, using a reward function that captures the temporal robustness of MITL specifications. Experiments on office-like environments demonstrate scalability and reveal trade-offs between horizon length, task count, and computation time, highlighting the practicality of the approach for real-world robotic routing with time-sensitive tasks.

Abstract

In environments like offices, the duration of a robot's navigation between two locations may vary over time. For instance, reaching a kitchen may take more time during lunchtime since the corridors are crowded with people heading the same way. In this work, we address the problem of routing in such environments with tasks expressed in Metric Interval Temporal Logic (MITL) - a rich robot task specification language that allows us to capture explicit time requirements. Our objective is to find a strategy that maximizes the temporal robustness of the robot's MITL task. As the first step towards a solution, we define a Mixed-integer linear programming approach to solving the task planning problem over a Varying Weighted Transition System, where navigation durations are deterministic but vary depending on the time of day. Then, we apply this planner to optimize for MITL temporal robustness in Markov Decision Processes, where the navigation durations between physical locations are uncertain, but the time-dependent distribution over possible delays is known. Finally, we develop a receding horizon planner for Markov Decision Processes that preserves guarantees over MITL temporal robustness. We show the scalability of our planning algorithms in simulations of robotic tasks.

Robust MITL planning under uncertain navigation times

TL;DR

The paper tackles robust task planning for robots under time-varying navigation durations by optimizing MITL temporal robustness. It first develops a MILP encoding for a to handle deterministic, time-dependent travel times, and then extends the framework to s to accommodate stochastic delays, including a receding-horizon planner that preserves robustness guarantees via worst-case lookahead. A two-stage MILP with history augmentation enables synthesis under uncertainty, using a reward function that captures the temporal robustness of MITL specifications. Experiments on office-like environments demonstrate scalability and reveal trade-offs between horizon length, task count, and computation time, highlighting the practicality of the approach for real-world robotic routing with time-sensitive tasks.

Abstract

In environments like offices, the duration of a robot's navigation between two locations may vary over time. For instance, reaching a kitchen may take more time during lunchtime since the corridors are crowded with people heading the same way. In this work, we address the problem of routing in such environments with tasks expressed in Metric Interval Temporal Logic (MITL) - a rich robot task specification language that allows us to capture explicit time requirements. Our objective is to find a strategy that maximizes the temporal robustness of the robot's MITL task. As the first step towards a solution, we define a Mixed-integer linear programming approach to solving the task planning problem over a Varying Weighted Transition System, where navigation durations are deterministic but vary depending on the time of day. Then, we apply this planner to optimize for MITL temporal robustness in Markov Decision Processes, where the navigation durations between physical locations are uncertain, but the time-dependent distribution over possible delays is known. Finally, we develop a receding horizon planner for Markov Decision Processes that preserves guarantees over MITL temporal robustness. We show the scalability of our planning algorithms in simulations of robotic tasks.
Paper Structure (16 sections, 1 theorem, 16 equations, 4 figures, 2 tables)

This paper contains 16 sections, 1 theorem, 16 equations, 4 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Notation
  3. Strategy Synthesis under Deterministic Navigation Times
  4. Approach
  5. Encoding of the VWTS \ref{['eq:main_ts_constraint']}
  6. Encoding of MITL constraints \ref{['eq:main_mtl_constraint']}
  7. Encoding of MITL temporal robustness \ref{['eq:main_problem_cost']}
  8. Strategy Synthesis under Uncertain Navigation Times
  9. Problem Definition and Approach
  10. A reward function for MITL temporal robustness
  11. Solving the MDP
  12. Planning with a receding horizon
  13. Experiments
  14. Deterministic Navigation Times
  15. Uncertain Navigation Times
  16. ...and 1 more sections

Key Result

Lemma IV.1

Solving the LP with $\bar{R}(\tilde{s})$ returns the worst-case temporal robustness that could be achieved after any number of future, receding horizon replannings.

Figures (4)

  • Figure 1: VWTS $\mathcal{A} = (S, s_0, \delta, \Pi, L, \Delta)$ shows a simplified office-like environment. States are labelled by $L=\{"\textit{exit}","\textit{off1}","\textit{off2}","\textit{lab}","\textit{kitc}"\}$. Self-transitions are not shown but are assumed to have a weight of 1, and transition weights are bidirectional. Transition weights are shown along the edges, and change based on time.
  • Figure 2: MDP $\mathcal{M}=(S, A, P, T, \Pi, L)$ is simplified example with 3 states. Probabilistic transitions are shown by the tables next to each edge. Here, transitions are time-independent, but our model allows for time-dependent transitions as well.
  • Figure 3: Reachable states of the MDP from Fig. \ref{['fig:figure_mdpsl']} after three transitions.
  • Figure 4: Transition system of an office-like environment. Labels and self-transitions are omitted for readability. Transitions are bi-directional. For more details, see our repositorygh_repo.

Theorems & Definitions (3)

  • Example 1
  • Lemma IV.1
  • proof