Title: Theory / Unimportant / CS / Fundamental / Model Checking / MTL / Taming the complexity of timeline-based planning

Definition: Timeline-based planning
Page: 1
Abbreviation: TP

Definition: The set of intervals of \(\mathbb R_+\) with bounds in \(\mathbb N\cup\{\infty\}\)
Page: 3
Section: 2
Notation: Intv

Name: A state variable
Definition: \(V_x\) a finite domain
Page: 3
Section: 2
Context: TP
Definition2: \(T_x:V_x\to 2^{V_x}\) value transition function
Definition3: \(D_x:V_x\to Intv\) constraint function
DefType: The tuple

Name: A token for \(x\)
Definition: \((v,d)\in V_x\times\mathbb R_+\) with \(d\in D_x(v)\)
Page: 3
Section: 2
Variables: \(x=(X_x,T_x,D_x)\) a state variable
Context: TP

Definition: \(v\)
Page: 3
Section: 2
Variables: \(x=(X_x,T_x,D_x)\) a state variable
\(t=(v,d)\) a token
Context: TP
Notation: \(value(t)\)

Name: A timeline of \(x\)
Definition: \((v_0,d_0),\dots,(v_n,d_n)\) a sequence of tokens such that \(v_{i+1}\in T_x(v_i)\)
Page: 3
Section: 2
Variables: \(x=(X_x,T_x,D_x)\) a state variable
Context: TP
Denoted by: \(\pi\)

Name: The start time of the \(i\)-th token
Definition: \(\sum_{h=0}^{i-1}d_h\)
Page: 3
Section: 2
Variables: \(x=(X_x,T_x,D_x)\) a state variable
\(\pi=(v_0,d_0),\dots,(v_n,d_n)\) a timeline for \(x\)
Context: TP
Notation: \(\mathbf s(\pi,i)\)

Name: The end time of the \(i\)-th token
Definition: \(\sum_{h=0}^{i}d_h\)
Page: 3
Section: 2
Variables: \(x=(X_x,T_x,D_x)\) a state variable
\(\pi=(v_0,d_0),\dots,(v_n,d_n)\) a timeline for \(x\)
Context: TP
Notation: \(\mathbf e(\pi,i)\)

Definition: A finite set of state variable
Page: 3
Section: 2
Context: TP
Denoted by: SV

Name: A multi-timeline of \(SV\)
Definition: A mapping from state variable \(x\in SV\) to a timeline for \(x\)
Page: 3
Section: 2
Variables: SV a finite set of state variable
Context: TP
Denoted by: \(\Pi\)

Name: A time-point constraints
Definition: A constraints on the start/end-times of tokens
Page: 4
Section: 2
Variables: SV a finite set of state variable
Context: TP

Name: An interval constraints
Definition: A constraints on the difference between start/end-times of tokens
Page: 4
Section: 2
Variables: SV a finite set of state variable
Context: TP

Name: An interval atom
Definition: A clause of the form \(o_i\le_{I}^{e_1,e_2}o_2\) with \(o_1,o_2\in\Sigma\), \(I\in Intv\), \(e_1,e_2\in\{\mathbf{s,e}\}\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of token names
Context: TP
Index: 3
Kind: Def
Example: the token associated with \(\overlineo\) occurs during the token associated with \(o\);
Applied to: \(o\le_{[0,\infty)}^{s,s}\overline o\land\overline o\le_{[0,\infty)}^{e,e}o\)

Name: A time-point atom
Definition: A clause of the form \(o_1\le_{I}^{e_1}n\) or \(n\le_{I}^{e_1}o_1\)with \(o_1\in\Sigma\), \(n\in\mathbb N\) \(I\in Intv\), \(e_1\in\{\mathbf{s,e}\}\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of token names
Context: TP
Index: 3
Kind: Def

Name: An existential statement for \(SV\)
Definition: A statement of the form \(\exists o_1[x_1=v_1]\dots\exists o_n[x_n=v_n)\bigwedge_{i}c_i\) with \(c_i\) interval or time-point atoms, \(o_i\in\Sigma\), \(x_i\in SV\), \(v_i\in V_{x_i}\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of token names
Context: TP
Index: 3
Kind: Def
Abbreviation: \(\mathcal E\)

Name: A quantifier
Definition: An element of the form \(o_i[x_i=v_i]\) with \(o_i\in\Sigma\), \(x_i\in SV\), \(v_i\in V_{x_i}\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
Context: TP
Index: 3
Kind: Def

Name: A free token
Definition: A token name used in \(\mathcal C\) but not occurring in any quantifier
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of tokens
\(\mathcal E=\exists o_1[x_1=v_1]\dots\exists o_n[x_n=v_n]\bigwedge_{i}c_i\) an existential statement for SV
Context: TP
Index: 3
Kind: Def

Name: A \(\Sigma\)-assignment for \(\Pi\)
Definition: A mapping from token \(o\in\Sigma\) a pair \((\pi,i)\) with \(\pi\) a timeline of \(\Pi\) and [$]0\le i<\abs{\pi}[/$] a position along \(\pi\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of tokens
\(\Pi\) a multi-timeline of \(SV\)
Context: TP
Index: 3
Kind: Def
Denoted by: \(\lambda_{\Pi}\)

Name: The interval atom \(o_1\le_{I}^{e_1,e_2}o_2\) is satisfied by \(\lambda_\Pi\)
Definition: \(e_2(\lambda_\Pi(o_2))-e_1(\lambda_\Pi(o_1))\in I\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of tokens
\(\Pi\) a multi-timeline of \(SV\)
\(\lambda_{\Pi}\) a \(\Sigma\)-assignment for \(\Pi\)
\(o_1,o_2\in\Sigma\)
\(e_1,e_2\in\mathbf\{s,e\}\)
\(I\in intv\)
Context: TP
Index: 3
Kind: Def

Name: The time-point atom \(o_1\le_{I}^{e_1}n\) is satisfied by \(\lambda_\Pi\)
Definition: \(n-e_1(\lambda_\Pi(o_1))\in I\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of tokens
\(\Pi\) a multi-timeline of \(SV\)
\(\lambda_{\Pi}\) a \(\Sigma\)-assignment for \(\Pi\)
\(o_1\in\Sigma\)
\(e_1\in\mathbf\{s,e\}\)
\(n\in\mathbb N\)
\(I\in intv\)
Context: TP
Index: 3
Kind: Def

Name: \(\lambda_\Pi\) is consistent with \(\mathcal E\)
Definition: for each quantified token name \(o_i\), \(\lambda_\Pi(o_i)=(\pi,h)\) where \(\pi=\Pi(x_i)\) and the \(h\)-th token of \(\pi\) has value \(v_i\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of tokens
\(\mathcal E=\exists o_1[x_1=v_1]\dots\exists o_n[x_n=v_n]\bigwedge_{i}c_i\) an existential statement for SV
Context: TP
Index: 3
Kind: Def

Name: \(\Pi\) satisfies \(\mathcal E\)
Definition: there exists a \(\Sigma\)-assignment for \(\Pi\) consistent with \(\mathcal E\) and satisfying each atom \(c_i\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of tokens
\(\mathcal E=\exists o_1[x_1=v_1]\dots\exists o_n[x_n=v_n]\bigwedge_{i}c_i\) an existential statement for SV
\(\Pi\) a multi-timeline of SV
Context: TP
Index: 3
Kind: Def

Name: A trigger
Definition: \(o_0[x_0=v_0]\) with \(o_0\in\Sigma\), \(x_0\in SV\), \(v_0\in V_{x_0}\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
Context: TP
Kind: Def

Name: A trigger-less rule
Definition: \(\top\to\bigvee_{i=1}^k\mathcal E_i\) with \(\mathcal E_i\) an existential statement without free token
Page: 4
Section: 2
Variables: SV a finite set of state variable
Context: TP
Kind: Def
Intuition: Initial condition or goal

Name: A trigger rule
Definition: \(o_0[x_0=v_0]\to \bigvee_{i=1}^k\mathcal E_i\) with \(\mathcal E_i\) an existential statement, \(o_0\in\Sigma\), \(x_0\in SV\), \(v_0\in V_{x_0}\) where the only possible free token is \(o_0\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
Context: TP
Kind: Def
Intuition: Useful to specify invariants and response requirements

Name: A synchronization rule
Definition: Either a trigger rule or a trigger-less rule
Page: 4
Section: 2
Variables: SV a finite set of state variable
Context: TP
Kind: Def
Denoted by: \(\mathcal R\)

Name: \(\Pi\) satisfies \(\mathcal R\)
Definition: \(\Pi\) satisfies some \(\mathcal E_i\)
Page: 4
Section: 2
Variables: SV a finite set of state variable
\(\mathcal R=\top\to\bigvee_{i=1}^k\mathcal E_i\) a triger-less rule
\(\Pi\) a multi-timeline of SV
Context: TP
Kind: Def

Name: A weakly-minimal in the future \(\Sigma\)-assignment w.r.t. \(o\)
Definition: for each \(o'\in\sigma\) with \(\lambda_\Pi(o')=(\pi,i)\), if \(\mathbf s(\pi_i)\ge\mathbf s(\lambda_\Pi(o))\) then there is no position \(l\) along the timeline \(\pi\) such that \(value(\pi(i))=value(\pi(l))\) and \(\mathbf s(\pi_i)>\mathbf s(\pi,l)\ge\mathbf s(\lambda_\Pi(o))\)
Page: 6
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of triggers
\(\Pi\) a multi-timeline of SV
\(o\in\Sigma\)
Context: TP
Kind: Def
DefType: A \(\Sigma\)-assignment \(\lambda_\Pi\)

Name: A weakly-minimal in the past \(\Sigma\)-assignment w.r.t. \(o\)
Definition: for each \(o'\in\sigma\) with \(\lambda_\Pi(o')=(\pi,i)\), if \(\mathbf s(\pi_i)\le\mathbf s(\lambda_\Pi(o))\) then there is no position \(l\) along the timeline \(\pi\) such that \(value(\pi(i))=value(\pi(l))\) and \(\mathbf s(\pi_i)<\mathbf s(\pi,l)\le\mathbf s(\lambda_\Pi(o))\)
Page: 6
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of triggers
\(\Pi\) a multi-timeline of SV
\(o\in\Sigma\)
Context: TP
Kind: Def
DefType: A \(\Sigma\)-assignment \(\lambda_\Pi\)

Name: A weakly-minimal \(\Sigma\)-assignment w.r.t. \(o\)
Definition: A \(\Sigma\)-assignment, weakly-minimal for the past and for the future w.r.t. \(o\)
Page: 6
Section: 2
Variables: SV a finite set of state variable
\(\Sigma\) an alphabet of triggers
\(\Pi\) a multi-timeline of SV
\(o\in\Sigma\)
Context: TP
Kind: Def

Name: \(\Pi\) satisfies \(\mathcal R\) for the weak (strong)-minimal semantic
Definition: \(\Pi\) satisfies some \(\mathcal E_i\) where \(\lambda_\Pi\) is existentially quantified over weakly (strongly) minimal w.r.t. the trigger token \(o_0\)
Page: 6
Section: 2
Variables: SV a finite set of state variable
\(\mathcal R=\top\to\bigvee_{i=1}^k\mathcal E_i\) a triger-less rule
\(\Pi\) a multi-timeline of SV
Context: TP
Index: 4
Kind: Def

Name: A TP domain
Definition: \(SV\) a finite set of state variable
Page: 6
Section: 2
Context: TP
Kind: Def
Definition2: \(R\) a finite set of synchronization rules
Denoted by: \(P\)
DefType: A pair

Name: A plan of \(P\)
Definition: A multi-timeline of \(SV\) satisfying all the rules in \(R\)
Page: 6
Section: 2
Variables: \(P=(SV,R)\) a TP domain
Kind: Def

Name: A weak (strong) minimal plan of \(P\)
Definition: A plan of \(P\) which is weak (strong) minimal semantics of trigger rules
Page: 6
Section: 2
Variables: \(P=(SV,R)\) a TP domain
Kind: Def

Page: 6
Section: 2
Returns: whether there is a weak minimal plan of \(P\)
Variables: \(P=(SV,R)\) a TP domain
Name: The weak minimal TP problem
Kind: Def

Page: 6
Section: 2
Name: The strong minimal TP problem
Time complexity: Undecidable
Returns: whether there is a strong minimal plan of \(P\)
Input: \(P=(SV,R)\) a TP domain
Kind: Def