Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesis of Timeline-Based Planning Strategies Avoiding Determinization

Renato Acampora, Dario Della Monica, Luca Geatti, Nicola Gigante, Angelo Montanari, Pietro Sala

TL;DR

This paper identifies a large fragment of qualitative timeline-based planning whose plan-existence problem can be directly mapped into the nonemptiness problem of deterministic finite automata, which can then be exploited to synthesize strategies.

Abstract

Qualitative timeline-based planning models domains as sets of independent, but interacting, components whose behaviors over time, the timelines, are governed by sets of qualitative temporal constraints (ordering relations), called synchronization rules. Its plan-existence problem has been shown to be PSPACE-complete; in particular, PSPACE-membership has been proved via reduction to the nonemptiness problem for nondeterministic finite automata. However, nondeterministic automata cannot be directly used to synthesize planning strategies as a costly determinization step is needed. In this paper, we identify a large fragment of qualitative timeline-based planning whose plan-existence problem can be directly mapped into the nonemptiness problem of deterministic finite automata, which can then be exploited to synthesize strategies. In addition, we identify a maximal subset of Allen's relations that fits into such a deterministic fragment.

Synthesis of Timeline-Based Planning Strategies Avoiding Determinization

TL;DR

This paper identifies a large fragment of qualitative timeline-based planning whose plan-existence problem can be directly mapped into the nonemptiness problem of deterministic finite automata, which can then be exploited to synthesize strategies.

Abstract

Qualitative timeline-based planning models domains as sets of independent, but interacting, components whose behaviors over time, the timelines, are governed by sets of qualitative temporal constraints (ordering relations), called synchronization rules. Its plan-existence problem has been shown to be PSPACE-complete; in particular, PSPACE-membership has been proved via reduction to the nonemptiness problem for nondeterministic finite automata. However, nondeterministic automata cannot be directly used to synthesize planning strategies as a costly determinization step is needed. In this paper, we identify a large fragment of qualitative timeline-based planning whose plan-existence problem can be directly mapped into the nonemptiness problem of deterministic finite automata, which can then be exploited to synthesize strategies. In addition, we identify a maximal subset of Allen's relations that fits into such a deterministic fragment.

Paper Structure

This paper contains 12 sections, 3 theorems, 5 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Background
  3. Timeline-Based Planning
  4. A Well-Behaved Fragment
  5. From Plans to Finite Words and Vice Versa
  6. DFA Accepting Plans
  7. DFA Accepting Solution Plans
  8. Blueprints, Snapshots, and Viewpoints
  9. States, Initial State, and Final States of AP
  10. Transition Function of AP
  11. A Maximal Subset of Allen's Relations
  12. Conclusions

Key Result

Lemma 1

Let $P = (\SV, S)$ be an eager qualitative timeline-based planning problem. Then, words accepted by $\mathcal{T}_{\SV}$ are exactly those encoding plans over . Moreover the size of $\mathcal{T}_{\SV}$ is at most exponential in the size of $P$.

Figures (1)

  • Figure 1: Above, we show the blueprint for the unique existential statement in the rule $a_0[x_0=v_0] \rightarrow \exists a_1[x_1=v_1]. (\mathop{\mathrm{start}}\nolimits(a_0) = \mathop{\mathrm{start}}\nolimits(a_1) \wedge \mathop{\mathrm{end}}\nolimits(a_0) \mathrel{\mathsf{\le}} \mathop{\mathrm{end}}\nolimits(a_1))$, from \ref{['sec:fragment']}. It forces token $a_0$ to either be a prefix of or coincide with token $a_1$. Below, the blueprint obtained replacing $\mathop{\mathrm{end}}\nolimits(a_0) \mathrel{\mathsf{\le}} \mathop{\mathrm{end}}\nolimits(a_1)$ with $\mathop{\mathrm{end}}\nolimits(a_0) \mathrel{\mathsf{<}} \mathop{\mathrm{end}}\nolimits(a_1)$, that forces $a_1$ to be a strict prefix of $a_1$.

Theorems & Definitions (12)

  • Definition 1: State variable
  • Definition 2: Tokens and timelines
  • Definition 3: Timeline-based planning problem
  • Definition 4: Plan and solution plan
  • Definition 5: Qualitative timeline-based planning
  • Definition 6: Eager rules
  • Definition 7: Words weakly-encoding plans
  • Lemma 1
  • Definition 8: Linearity condition
  • Lemma 2
  • ...and 2 more