Synthesis of timeline-based planning strategies avoiding determinization

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 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 synthesize strategies. In addition, we identify a maximal subset of Allen's relations that fits into such a deterministic fragment.

Figures (9)

• Figure 1: A (partial) plan satisfying the rule from Equation \ref{['eq:example-eager']}, which is eager, and the one from Equation \ref{['eq:example-2-eager']}, which is not. The token starting at time 1 triggers both rules. In both cases, the satisfaction of the rule is witnessed by the second token of value $v_1$ in the relevant timeline (not the first one). However, a DFA that behaves eagerly can be instructed to identify the witnessing token for the eager rule, but not for the non-eager one. Note that the token for $x_1$ starting at time 3 has value $v_2 \neq v_1$; thus, it does not match token name $a_1$, and cannot be used to fulfill the rule from Equation \ref{['eq:example-eager']}.
• Figure 2: Graphical representation of sets $W_n$, with $n \in \mathbb N$. $W_n$ includes words $\lambda=\sigma_0\sigma_1 \ldots \sigma_h$, for all even positive natural numbers $h$, encoding plans over $\mathsf{SV}\xspace_n$ and such that: the timeline associated with variable $x_0$ features $h/2$$v_0$-valued tokens and a final $\overline v_0$-valued token; timelines associated with variables other than $x_0$ feature an initial $\overline v_j$-valued token, followed by $h/2$ tokens labeled with either $v_j$ or $\overline v_j$, for $j \in [n]\xspace^{>0}\xspace$.
• Figure 3: The picture shows two DAGs on the left-hand side. The one on the top is associated with (the existential statement of) the rule $a_0[x_0=v_0] \rightarrow \exists a_1[x_1=v_1]. (\mathop{\mathrm{\tt s}}\nolimits(a_0) \mathrel{\mathsf{\le}} \mathop{\mathrm{\tt s}}\nolimits(a_1) \wedge \mathop{\mathrm{\tt s}}\nolimits(a_1) \mathrel{\mathsf{\le}} \mathop{\mathrm{\tt s}}\nolimits(a_0) \wedge \mathop{\mathrm{\tt e}}\nolimits(a_0) \mathrel{\mathsf{\le}} \mathop{\mathrm{\tt e}}\nolimits(a_1))$. It forces token $a_0$ to either be a prefix of or coincide with token $a_1$. The one on the bottom is associated with the existential statement obtained replacing $\mathop{\mathrm{\tt e}}\nolimits(a_0) \mathrel{\mathsf{\le}} \mathop{\mathrm{\tt e}}\nolimits(a_1)$ with $\mathop{\mathrm{\tt e}}\nolimits(a_0) \mathrel{\mathsf{<}} \mathop{\mathrm{\tt e}}\nolimits(a_1)$, that forces $a_0$ to be a (strict) prefix of $a_1$. The labeling function is the same for both DAGs, and it is shown on the right-hand side.
• Figure 4: The automaton $\mathcal{A}_{P}\xspace$ for the non-strict rule whose DAG is depicted in \ref{['fig:dag-begin-strict-nonstrict']} (non-strict), with four non-sink states.
• Figure 5: The automaton $\mathcal{A}_{P}\xspace$ for the strict rule whose DAG is depicted in \ref{['fig:dag-begin-strict-nonstrict']} (strict), with six non-sink states.

Theorems & Definitions (42)

• Definition 2.1: State variable
• Definition 2.2: Token and timeline
• Definition 2.3: Timeline-based planning problem
• Definition 2.4: Plan and solution plan
• Definition 2.5: Qualitative timeline-based planning
• Definition 3.1: Ambiguous token, eager rule, eager planning problem
• Definition 4.1: Words weakly-encoding plans
• Proposition 5.1
• proof
• Proposition 5.2