*A preliminary version of this article has appeared in the proceedings of GandALF 2022 [AGG+22].

[a] [a] [b] [a] [c]

# Controller Synthesis for Timeline-based Games*

Renato Acampora  ,  Luca Geatti  ,  Nicola Gigante  ,  Angelo Montanari  and
Valentino Picotti  University of Udine, Italy<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>Free University of Bozen-
Bolzano, Italy<EMAIL_ADDRESS>University of Southern Denmark
<EMAIL_ADDRESS>
###### Abstract.

In the timeline-based approach to planning, the evolution over time of a set
of state variables (the timelines) is governed by a set of temporal
constraints. Traditional timeline-based planning systems excel at the
integration of planning with execution by handling _temporal uncertainty_. In
order to handle general nondeterminism as well, the concept of _timeline-based
games_ has been recently introduced. It has been proved that finding whether a
winning strategy exists for such games is $\mathsf{2EXPTIME}$-complete.
However, a concrete approach to synthesize controllers implementing such
strategies is missing. This article fills the gap by providing an effective
and computationally optimal approach to controller synthesis for timeline-
based games.

###### Key words and phrases:

Planning, automata, synthesis

##  1\. Introduction

Automated planning is the field of _artificial intelligence_ that studies the
development of autonomous agents able of reasoning about how to reach some
goals, starting from a high-level description of their operating environment.
It is one of the most studied fields of AI, with early work going several
decades back [MH69, FN71]. Most of the research by the planning community
focuses on the _action-based_ approach, where planning problems are modeled in
terms of _actions_ that an agent has to perform to suitably change its
_state_. The task is to devise a sequence of such actions that lead to the
goal when executed starting from a given initial state [FN71, FL03].

In this paper, we focus on the alternative paradigm of _timeline-based
planning_ , an approach born and developed in the space sector [Mus94]. In
timeline-based planning, there is no explicit separation among actions,
states, and goals. Planning domains are represented as systems of independent
but interacting components, whose behavior over time, the _timelines_ , is
governed by a set of temporal constraints, called _synchronization rules_.

Over the years, timeline-based planning systems have been developed and
successfully exploited by space agencies on both sides of the Atlantic
[CCF+06, CCD+07, FJ03, BS07, CRK+00], for short- to long-term mission planning
[CRT+15] as well as on-board autonomy [FCO+11]. The main advantage of such a
paradigm in these contexts is the ability of these systems of handling both
planning and _execution_ in a uniform way: by the use of _flexible timelines_
, timeline-based planners can produce robust plans that, during execution, can
be adapted to the current contingency.

However, flexible timelines currently employed in timeline-based systems only
handle _temporal uncertainty_ , where the precise timings of events in the
plan are unknown, but the causal sequence of the events is determined. In
particular, they cannot generate robust plans against an environment empowered
with general _nondeterminism_. To overcome this limitation, the concept of
_timeline-based games_ was recently introduced [GMO+20]. In timeline-based
games, state variables belong either to the controller or to the environment.
The controller aims at satisfying its set of _system_ rules, while the
environment can make arbitrary moves, as long as the _domain_ rules that
define the game arena are satisfied. A controller’s strategy is winning if it
guarantees that the controller wins, regardless of the choices made by the
environment. The moves available to the two players can determine both _what_
happens and _when_ it happens, thus handling temporal uncertainty and general
nondeterminism in a uniform way.

Determining whether a winning strategy exists for timeline-based games has
been proved to be $\mathsf{2EXPTIME}$-complete [GMO+20]. However, there is
currently no effective way to synthesize a controller that implements such
strategies. A necessary condition for synthesizing a finite-state strategy and
the corresponding controller is the availability of a _deterministic_ arena.
Two methods to obtain such an arena have been followed in the literature, but
both have limitations and turn out to be inadequate. On the one hand, the
complexity result of [GMO+20] relies on the construction of a (doubly
exponential) _concurrent game structure_ used to model check some Alternating-
time Temporal Logic formulas [AHK02]. Even though such a structure is
deterministic and theoretically suitable to solve a reachability game and to
synthesize a controller, its construction relies on theoretical
nondeterministic procedures that are not realistically implementable. On the
other hand, Della Monica et al. [DGMS18] devised an automata-theoretic
solution that provides a concrete and effective way to construct an automaton
that accepts a word if and only if the original planning problem has a
solution plan. Unfortunately, the size of the resulting _nondeterministic_
automaton is already doubly exponential, and its determinization would result
in a further blowup and thus in a non-optimal procedure.

The present paper fills the gap by developing an effective and computationally
optimal approach to synthesizing controllers for timeline-based games. The
proposed method addresses the limitations of previous techniques by directly
constructing a _deterministic_ finite-state automaton of an optimal doubly-
exponential size, that recognizes solution plans. Such an automaton can be
turned into the arena for a reachability game, for which many controller
synthesis techniques are available in the literature. The paper is a
significantly revised and extended version of [AGG+22]. It provides a detailed
account of the general framework, gives some illustrative examples, and fully
works out all the proofs.

The rest of the paper is organized as follows. After discussing related work
in Section 2, Section 3 introduces timeline-based planning and games. Section
4 presents the main technical contribution of the paper, namely, the
construction of the deterministic automaton that recognizes solution plans.
Section 5 shows how to turn such an automaton into the arena of a suitable
game from which the controller can be synthesized. Section 6 summarizes the
main contributions of the work and suggest future research directions. All the
technical proofs are included in the appendix.

##  2\. Related work

The paradigm of timeline-based planning has been first introduced to plan and
schedule scientific operations of the Hubble space telescope [Mus94]. In the
following two decades, many timeline-based planning systems have been
developed both at NASA and ESA, including EUROPA [BWMB+05], ASPEN [CRK+00],
and APSI [DPC+08]. Such systems have been used both for short- to long-term
mission planning, for the renowned Rosetta mission [CRT+15], and for onboard
autonomy [FCO+11]. Elements of the timeline-based and the action-based
paradigm have been combined into the Action Notation Modeling Language (ANML)
[SFC08], extensively used at NASA since then.

Despite the real-world success, the timeline-based planning paradigm lacked a
thorough foundational understanding in contrast to the action-based one, which
has been extensively studied from a theoretical perspective from the start
[MH69, Byl94]. To enable theoretical investigations into timeline-based
planning, Cialdea Mayer et al. [COU16] laid down the core features of the
paradigm, describing them in a uniform formalism, which has been later studied
in several contributions. The formalism was compared to traditional action-
based languages like STRIPS, and it was proved that the latter are expressible
by timeline-based languages [GMCO16]. The timeline-based plan existence
problem was proved to be $\mathsf{EXPSPACE}$-complete [GMCO17] over discrete
time in the general case, and $\mathsf{PSPACE}$-complete with qualitative
constraints only [DGTM20]. On dense time, the problem goes from being
$\mathsf{NP}$-complete to undecidable, depending on the applied syntactic
restrictions [BMM+20]. Additionally, logical [DGM+17] and automata-theoretic
[DGMS18] counterparts have been investigated to study the expressiveness of
timeline-based languages.

The above body of work focuses on _deterministic_ timeline-based planning
domains. However, the paradigm also fits to _uncertain_ domains requiring
robust plans. Current timeline-based planning systems employ the concept of
_flexible timelines_ , described as including uncertainty in the timings of
events, representing envelopes of possible executions of the plan. Planners,
when possible, produce _strongly controllable_ flexible plans, whose execution
is then robust for the given temporal uncertainty. In order to obtain
controllers for executing strongly controllable flexible plans, the problem
can be simplified by reducing it to _timed game automata_ [OFCF11].

While the current approach works fairly well in handling temporal uncertainty,
it does not support scenarios where the environment is fully nondeterministic.
Furthermore, as pointed out in [GMO+20], the language of timeline-based
planning as formalized in [COU16] allows one to write domains that are not
solvable by strongly controllable flexible plans, but that may easily be by
strategies coping with general nondeterminism. For this reason, [GMO+20]
introduced the concept of _timeline-based game_ , which is the focus of this
work. Timeline-based games adopt a game-theoretic point of view, where the
controller and the environment play by constructing timelines, with the
controller trying to fulfill its synchronization rules independently from the
choices of the environment. This setting allows one to handle both temporal
uncertainty and general nondeterminism, thus strictly generalizing previous
approaches based on flexible timelines. In [GMO+20], the problem of deciding
the existence of a winning strategy for a given timeline-based game has been
proved to be $\mathsf{2EXPTIME}$-complete. The proof is based on the
construction of a _concurrent game structure_ where a suitable _alternating-
time temporal logic_ (ATL) formula is model checked [AHK02]. However, the
construction relies on nondeterministic procedures that are not effectively
implementable, and thus it does not solve the problem of synthesizing actual
controllers for timeline-based games. This work fills the gap by providing an
effective synthesis algorithm.

The devised algorithm builds on classical results in the field of _reactive
synthesis_ , which studies how to build correct-by-construction controllers
satisfying high-level logical specifications. The original formulation of the
problem of reactive synthesis is due to Church [Chu62]. The problem for _S1S_
specifications was later solved by Büchi and Landweber using a non-elementary
complexity algorithm [BL90]. As for Linear Temporal Logic (LTL)
specifications, the problem is $\mathsf{2EXPTIME}$-complete [PR89b, Ros92],
which, interestingly, is the same complexity as timeline-based games. In both
cases, the core of the synthesis algorithm is the construction of a
_deterministic_ arena, where the game can be solved with a fix-point
computation. This work focuses on constructing such an arena for timeline-
based games (Sections 4 and 5).

##  3\. Preliminaries

In this section, we provide an overview of the general framework that
underpins our work. We begin by introducing the general features of timeline-
based planning, and then we discuss timeline-based games. Next, we introduce
the reactive synthesis problem. Finally, we recall the concept of _difference
bound matrices_ (DBMs) [Dil89, PH07], which are the data structures that we
will use to represent the temporal constraints of a system.

###  3.1. Timeline-based planning

The first basic notion is that of _state variable_. [State variable] A _state
variable_ is a tuple $x=(V_{x},T_{x},D_{x},\gamma)$, where:

  * •

$V_{x}$ is the _finite domain_ of $x$;

  * •

$T_{x}:V_{x}\to 2^{V_{x}}$ is the _value transition function_ of $x$, which
maps each value $v\in V_{x}$ to the set of values that can immediately follow
it;

  * •

$D_{x}:V_{x}\to\mathbb{N}\times\mathbb{N}$ is the _duration function_ of $x$,
mapping each value $v\in V_{x}$ to a pair
$(d^{x=v}_{min},d^{x=v}_{max\vphantom{i}})$ specifying respectively the
minimum and maximum duration of any interval where $x=v$;

  * •

$\gamma:V_{x}\to\\{\mathsf{c},\mathsf{u}\\}$ is the _controllability tag_ ,
that, for each value $v\in V_{x}$, specifies whether it is _controllable_
$\left(\gamma\left(v\right)=\mathsf{c}\right)$ or _uncontrollable_
$\left(\gamma\left(v\right)=\mathsf{u}\right)$.

A state variable $x$ takes its values from a finite domain and represents a
finite state machine with a transition function $T_{x}$. The behavior over
time of a state variable $x$ is modeled by a timeline. Intuitively, a
_timeline_ for a state variable $x$ is a finite sequence of tokens, that is,
contiguous time intervals where $x$ holds a given value.

Following the approach described in [GMO+20], instead of formally defining
timelines in terms of tokens, we represent executions of timeline-based
systems as single words, called _event sequences_ , where each event describe
the start/end of some token in a given time point.

To this end, we first define the notion of action.

Let $\mathsf{SV}$ be a set of state variables. An _action_ is a term of the
form $\operatorname{start}(x,v)$ or $\operatorname{end}(x,v)$, where
$x\in\mathsf{SV}$ and $v\in V_{x}$.

Actions of the form $\operatorname{start}(x,v)$ are _starting_ actions, and
those of the form $\operatorname{end}(x,v)$ are _ending_ actions. We denote by
$\mathsf{A}_{\mathsf{SV}}$ the set of all the actions definable over a set of
state variables $\mathsf{SV}$.

[Event sequence [GMO+20]] Let $\mathsf{SV}$ be a set of state variables and
$\mathsf{A}_{\mathsf{SV}}$ be the set of all the _actions_
$\operatorname{start}(x,v)$ and $\operatorname{end}(x,v)$, for
$x\in\mathsf{SV}$ and $v\in V_{x}$. An _event sequence_ over $\mathsf{SV}$ is
a sequence ${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ of
pairs ${\mu}_{i}=(A_{i},\delta_{i})$, called _events_ , where
$A_{i}\subseteq\mathsf{A}_{\mathsf{SV}}$ and $\delta_{i}\in\mathbb{N}^{+}$,
such that, for any $x\in\mathsf{SV}$:

  1. (1)

for all $1\leq i\leq n$, if $\operatorname{start}(x,v)\in A_{i}$, for some
$v\in V_{x}$, then there is no $\operatorname{start}(x,v^{\prime})$ in any
${\mu}_{j}$ before the closest event ${\mu}_{k}$, with $k>i$, such that
$\operatorname{end}(x,v)\in A_{k}$ (if any);

  2. (2)

for all $1\leq i\leq n$, if $\operatorname{end}(x,v)\in A_{i}$, for some $v\in
V_{x}$, then there is no $\operatorname{end}(x,v^{\prime})$ in any ${\mu}_{j}$
after the closest event ${\mu}_{k}$, with $k<i$, such that
$\operatorname{start}(x,v)\in A_{k}$ (if any);

  3. (3)

for all $1\leq i<n$, if $\operatorname{end}(x,v)\in A_{i}$, for some $v\in
V_{x}$, then $\operatorname{start}(x,v^{\prime})\in A_{i}$, for some
$v^{\prime}\in V_{x}$;

  4. (4)

for all $1<i\leq n$, if $\operatorname{start}(x,v)\in A_{i}$, for some $v\in
V_{x}$, then $\operatorname{end}(x,v^{\prime})\in A_{i}$, for some
$v^{\prime}\in V_{x}$.

The first two conditions guarantee correct parenthesis placement by
identifying the start and the end of each token in the sequence. Condition 1
prevents a token from starting before the end of the previous one, while
condition 2 prevents the occurrence of two consecutive ends not interleaved by
a start. Conditions 3 and 4 ensure seamless continuity: each token’s end
(resp., start) is consistently followed (preceded) by the start (resp., end)
of another, except for the first (resp., last) event in the sequence. These
latter conditions prevent gaps in the timeline description of the represented
plan.

In event sequences, a token for a variable $x$ is a maximal interval with at
most one occurrence of events ${\mu}_{i}=(A_{i},\delta_{i})$ and
${\mu}_{j}=(A_{j},\delta_{j})$, where $\operatorname{start}(x,v)\in A_{i}$ and
$\operatorname{end}(x,v)\in A_{j}$, for some $v\in V_{x}$. We say such a token
_starts_ at position $i$ and _ends_ at position $j$. Note that Section 3.1
implies that a token that has started is not required to end before the end of
the sequence and that it can end without the corresponding starting action
ever appearing. If this is the case, we say that an event sequence is _open_
either to the right or to the left. Otherwise, it is said to be _closed_. An
event sequence closed to the left and open to the right is called a _partial
plan_. Notice that the empty event sequence $\varepsilon$ is closed on both
sides for any variable. Furthermore, in closed event sequences, the first
event contains only start actions, while the last one contains only end
actions, one for each variable $x$.

Given an event sequence
${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ over a set of
state variables $\mathsf{SV}$, with ${\mu}_{i}=(A_{i},\delta_{i})$, we define
$\delta({\overline{\mu}})$ as $\sum_{1<i\leq n}\delta_{i}$, that is,
$\delta({\overline{\mu}})$ is the time elapsed from the start to the end of
the event sequence (its duration). For any subsequence
$\langle{\mu}_{i},\ldots,{\mu}_{j}\rangle$ of ${\overline{\mu}}$, abbreviated
${\overline{\mu}}_{[i\ldots j]}$, we denote by $\delta_{i,j}$ (or,
equivalently, $\delta({\overline{\mu}}_{[i\ldots j]})$) the amount of time
spanning that subsequence. Notice that $\delta_{i,j}$ is defined as
$\sum_{i<k\leq j}\delta_{k}$. Finally, given an event sequence
${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$, we define
${\overline{\mu}}_{<i}$ as $\langle{\mu}_{1},\ldots,{\mu}_{i-1}\rangle$, for
each $1<i\leq n$.

In timeline-based planning, the objective is to satisfy a set of
_synchronization rules_ , that specify the desired behavior of the system
(constraints and goal). These rules relate tokens, possibly belonging to
different timelines, through temporal relations among their endpoints. Let
$\mathsf{SV}$ be a set of state variables and $\mathsf{N}=\\{a,b,\ldots\\}$ be
a set of _token names_.

[Atom] An atom is a temporal relation between tokens’ endpoints of the form
$\langle\mathit{term}\rangle\mathrel{\mathsf{\leq}}_{[l,u]}\langle\mathit{term}\rangle$,
where $l\in\mathbb{N}$, $u\in\mathbb{N}\cup\\{+\infty\\}$, $l\leq u$, and a
_term_ is either $\operatorname{start}(a)$ or $\operatorname{end}(a)$, for
some $a\in\mathsf{N}$.

As an example, the atom
$\operatorname{start}(a)\mathrel{\mathsf{\leq}}_{[3,7]}\operatorname{end}(b)$
constrains token $a$ to start at least $3$ and at most $7$ time units before
the end of token $b$, while the atom
$\operatorname{start}(a)\mathrel{\mathsf{\leq}}_{[0,+\infty]}\operatorname{start}(b)$
simply constrains token $a$ to start before token $b$.

[Synchronization rule] A synchronization rule $\mathsf{R}$ has one of the
following two forms:

$\displaystyle\begin{array}[]{rcl}\@add@centering\centering\langle
rule\rangle&:=&a_{0}[x_{0}=v_{0}]\rightarrow\langle body\rangle\\\ \langle
rule\rangle&:=&\top\rightarrow\langle body\rangle\\\ \langle
body\rangle&:=&\mathsf{E}_{1}\lor\mathsf{E}_{2}\lor\dots\lor\mathsf{E}_{k}\\\
\mathsf{E}_{j}&\vcentcolon=&\exists a_{1}[x_{1}=v_{1}]a_{2}[x_{2}=v_{2}]\ldots
a_{n}[x_{n}=v_{n}]\mathrel{.}\mathsf{C}_{j},\ for\ 1\leq j\leq k,\end{array}$

where $a_{i}\in\mathsf{N}$, $x_{i}\in\mathsf{SV}$, $v_{i}\in V_{x_{i}}$, and
$\mathsf{C}_{j}$ is a conjunction of atoms, for $0\leq i\leq n$. Terms
$a_{i}[x_{i}=v_{i}]$ are referred to as _quantifiers_. The term
$a_{0}[x_{0}=v_{0}]$ is called the _trigger_. The disjuncts in the body are
called _existential statements_. Quantifiers refer to tokens with the
corresponding variable and value. The intuitive semantics of a synchronization
rule can be given as follows: for every token satisfying the trigger, at least
one of the existential statements must be satisfied as well. Each existential
statement $\mathsf{E}_{j}$ requires the existence of tokens that satisfy the
quantifiers in its prefix and the clause $\mathsf{C}_{j}$. A token that
satisfies the trigger of a rule is said to _trigger_ that rule. The trigger of
a rule can be empty ($\top$). In such a case, the rule is referred to as
_triggerless_ and it requires the satisfaction of its body without any
precondition.

Let $a$ and $b$ be token names. Here are two examples of synchronization rules
(relations $=$ and $\mathrel{\mathsf{\leq}}$ are syntactic sugar for
$\mathrel{\mathsf{\leq}}_{[0,0]}$ and $\mathrel{\mathsf{\leq}}_{[0,+\infty]}$,
respectively):

$\displaystyle a[x_{s}=\mathsf{Comm}]\rightarrow{}$ $\displaystyle\exists
b[x_{g}=\mathsf{Available}]\mathrel{.}\operatorname{start}(b)\mathrel{\mathsf{\leq}}\operatorname{start}(a)\land\operatorname{end}(a)\mathrel{\mathsf{\leq}}\operatorname{end}(b)$
$\displaystyle a[x_{s}=\mathsf{Science}]\rightarrow{}$ $\displaystyle\exists
b[x_{s}=\mathsf{Slewing}]\ c[x_{s}=\mathsf{Earth}]\
d[x_{s}=\mathsf{Comm}]\mathrel{.}{}$
$\displaystyle\operatorname{end}(a)=\operatorname{start}(b)\land\operatorname{end}(b)=\operatorname{start}(c)\land\operatorname{end}(c)=\operatorname{start}(d)$

where variables $x_{s}$ and $x_{g}$ represent the state of a spacecraft and
the visibility of the communication ground station, respectively. The first
synchronization rule requires the satellite and the ground station to
coordinate their communications so that when the satellite is transmitting,
the ground station is available for reception. The second one instructs the
system to send data to Earth after every measurement session, interleaved by
the required slewing operation. Triggerless rule can be used to state the
_goal_ of the system. As an example, the following rule ensures that the
spacecraft performs some scientific measurement:

$\top\rightarrow\exists a[x_{s}=\mathsf{Science}]$

Triggerless rules only require the existence of tokens specified by the
existential statements, being their universal quantification trivial. In fact,
they are syntactic sugar, as it is possible to translate them into triggered
rules, as shown in [GMO+20]. From now on, we will not consider them anymore.

We now formalise the above intuitive account of the semantics of
synchronization rules. [Matching functions [Gig19]] Let
${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ be a (possibly
open) event sequence, $\mathsf{E}\equiv\exists a_{1}[x_{1}=v_{1}]\ldots
a_{k}[x_{k}=v_{k}]\mathrel{.}\mathsf{C}$ be one of the existential statements
of a synchronization rule $\mathsf{R}\equiv
a_{0}[x_{0}=v_{0}]\rightarrow\mathsf{E}_{1}\lor\ldots\lor\mathsf{E}_{m}$, and
$V$ be a set of terms such that $\operatorname{start}(a)\in V$ or
$\operatorname{end}(a)\in V$ only if $a\in\\{a_{0},\ldots,a_{k}\\}$. A
_matching function_ $\gamma:V\to[1,\ldots,n]$ maps each term $T\in V$ to an
event ${\mu}_{\gamma(T)}$ in ${\overline{\mu}}$, such that:

  1. (1)

for each $T\in V$, with $T=\operatorname{start}(a)$ (resp.,
$T=\operatorname{end}(a)$), if $a$ is quantified as $a[x=v]$ in $\mathsf{E}$,
then the event ${\mu}_{\gamma(T)}=(A_{T},\delta_{T})$ is such that
$\operatorname{start}(x,v)\in A_{T}$ (resp., $\operatorname{end}(x,v)\in
A_{T}$);

  2. (2)

if both $T=\operatorname{start}(a)$ and $T^{\prime}=\operatorname{end}(a)$
belong to $V$ for some token name $a\in\mathsf{N}$, then $\gamma(T)$ and
$\gamma(T^{\prime})$ identify the endpoints of the same token.

As a matter of fact, in [Gig19], matching functions are defined in terms of
_rule graphs_ , a data structure that we do not use here. For this reason, we
reformulated the original definition in terms of event sequences.

The following definition gives a formal account of the semantics of
synchronization rules. [Semantics of synchronization rules] Let
$\mathsf{R}\equiv
a_{0}[x_{0}=v_{0}]\rightarrow\mathsf{E}_{1}\lor\ldots\lor\mathsf{E}_{m}$ and
let ${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ be an event
sequence. We say that $\mathsf{R}$ is _satisfied_ by ${\overline{\mu}}$ if,
_for each_ event ${\mu}_{i}=(A_{i},\delta_{i})$ such that
$\operatorname{start}(x_{0},v_{0})\in A_{i}$, there exist an existential
statement $\mathsf{E}_{j}\equiv\exists a_{1}[x_{1}=v_{1}]\ldots
a_{k}[x_{k}=v_{k}]\mathrel{.}\mathsf{C}$ and a matching function $\gamma$ such
that if $T\leq_{[l,u]}T^{\prime}$ appears in $\mathsf{C}$, then
$l\leq\gamma(T^{\prime})-\gamma(T)\leq u$, for any pair of terms $T$ and
$T^{\prime}$.

_Timeline-based planning problems_ can be defined as follows. [Timeline-based
planning problem] A _timeline-based planning problem_ is a pair
$P=(\mathsf{SV},\mathsf{S})$, where $\mathsf{SV}$ is a set of state variables
and $\mathsf{S}$ is a set of synchronization rules over $\mathsf{SV}$. An
event sequence ${\overline{\mu}}$ over $\mathsf{SV}$ is a solution plan for
$P$ if all the rules in $\mathsf{S}$ are satisfied by ${\overline{\mu}}$.

###  3.2. Timeline-based games.

We are now ready to introduce the notion of _timeline-based game_ , that
subsumes that of _timeline-based planning with uncertainty_ given in [COU16].

[Timeline-based game] A _timeline-based game_ is a tuple
$G=(\mathsf{SV}_{C},\mathsf{SV}_{E},\mathsf{S},$ $\mathsf{D})$, where
$\mathsf{SV}_{C}$ and $\mathsf{SV}_{E}$ are the sets of _controlled_ and
_external_ state variables, respectively, and $\mathsf{S}$ and $\mathsf{D}$
are the sets of _system_ and _domain_ synchronization rules, respectively,
both involving variables from $\mathsf{SV}_{C}$ and $\mathsf{SV}_{E}$.

A partial plan for $G$ is a partial plan over the variables
$\mathsf{SV}_{C}\cup\mathsf{SV}_{E}$. Let ${\Pi}_{G}$ be the set of all
possible partial plans for $G$, simply ${\Pi}$ when there is no ambiguity.
Since the empty event sequence $\varepsilon$ is closed and
$\delta(\varepsilon)=0$, the _empty_ partial plan $\varepsilon$ is a good
starting point for the game. Players incrementally build onto a partial plan,
starting from $\varepsilon$, by playing actions that specify which tokens to
start and (or) to end, adding an event that extends the event sequence, or
complementing the existing last one.

Formally, we partition the set of all the available actions
$\mathsf{A}_{\mathsf{SV}}$ into those that are playable by either of the two
players.

[Partition of player actions] Let
$\mathsf{SV}=\mathsf{SV}_{C}\cup\mathsf{SV}_{E}$. The set
$\mathsf{A}_{\mathsf{SV}}$ of available actions over $\mathsf{SV}$ is
partitioned into the sets $\mathsf{A}_{C}$ of _Charlie_ ’s actions and
$\mathsf{A}_{E}$ of _Eve_ ’s actions, which are defined as follows:

$\displaystyle\mathsf{A}_{C}={}$
$\displaystyle\underbrace{\\{\operatorname{start}(x,v)\mathrel{|}x\in\mathsf{SV}_{C},\;v\in
V_{x}\\}}_{\text{start tokens on \emph{Charlie}'s
timelines}}\;\cup\;\underbrace{\\{\operatorname{end}(x,v)\mathrel{|}x\in\mathsf{SV},\;v\in
V_{x},\;\gamma_{x}(v)=\mathsf{c}\\}}_{\text{end controllable tokens}}$ (1)
$\displaystyle\mathsf{A}_{E}={}$
$\displaystyle\underbrace{\\{\operatorname{start}(x,v)\mathrel{|}x\in\mathsf{SV}_{E},\;v\in
V_{x}\\}}_{\text{start tokens on \emph{Eve}'s
timelines}}\;\cup\;\underbrace{\\{\operatorname{end}(x,v)\mathrel{|}x\in\mathsf{SV},\;v\in
V_{x},\;\gamma_{x}(v)=\mathsf{u}\\}}_{\text{end uncontrollable tokens}}$ (2)

Hence, players can start tokens for owned variables and end them for values
that they control. Let $d=\max(L,U)+1$, where $L$ and $U$ are the maximum
lower and (finite) upper bounds appearing in any rule of $G$. Note that, by
Section 3.2, we may have $x\in\mathsf{SV}_{E}$ and $\gamma_{x}(v)=c$ for some
$v\in V_{x}$. This means that Charlie may control the duration of a variable
that belongs to Eve. This situation is symmetrical to the more common one
where Eve controls the duration of a variable that belongs to Charlie, that
is, uncontrollable tokens. As an example, Charlie may decide to start a task,
without being able to foresee how long it will take. Similarly, the
environment may trigger the start of a process, fixing a plant fault, but
Charlie may be able to control, to some extent, how long it will take to end
it, we can decide to fix it today or tomorrow.

Actions combine into _moves_ starting (resp., ending) multiple tokens
simultaneously.

[Move] A _move_ ${\mu}_{C}$ for _Charlie_ is a term of the form
$\operatorname{wait}(\delta_{C})$ or $\operatorname{play}(A_{C})$, where
$1\leq\delta_{C}\leq d$ and $\varnothing\neq A_{C}\subseteq\mathsf{A}_{C}$ is
either a set of _starting_ actions or a set of _ending_ actions. A _move_
${\mu}_{E}$ for _Eve_ is a term of the form $\operatorname{play}(A_{E})$ or
$\operatorname{play}(\delta_{E},A_{E})$, where $1\leq\delta_{E}\leq d$ and
$A_{E}\subseteq\mathsf{A}_{E}$ is either a set of _starting_ actions or a set
of _ending_ actions. By Section 3.2, moves like $\operatorname{play}(A_{C})$
and $\operatorname{play}(\delta_{E},A_{E})$ can play either
$\operatorname{start}(x,v)$ actions only or $\operatorname{end}(x,v)$ actions
only. A move of the former kind is called a _starting_ move, while a move of
the latter kind is called an _ending_ move. We consider $\operatorname{wait}$
moves as _ending_ moves. Starting and ending moves must alternate during the
game.

Let us denote the sets of _Charlie_ ’s and _Eve_ ’s moves by $\mathcal{M}_{C}$
and $\mathcal{M}_{E}$ , respectively. A round of the game is defined as
follows.

[Round] A _round_ ${\rho}$ is a pair
$({\mu}_{C},{\mu}_{E})\in\mathcal{M}_{C}\times\mathcal{M}_{E}$ of moves such
that:

  1. (1)

${\mu}_{C}$ and ${\mu}_{E}$ are either both _starting_ or both _ending_ moves;

  2. (2)

either ${\rho}=(\operatorname{play}(A_{C}),\operatorname{play}(A_{E}))$, or
${\rho}=(\operatorname{wait}(\delta_{C}),\operatorname{play}(\delta_{E},A_{E}))$,
with $\delta_{E}\leq\delta_{C}$;

A _starting_ (resp., _ending_) round is one made of starting (resp., ending)
moves. Since _Charlie_ cannot play empty moves and $\operatorname{wait}$ moves
are ending moves, each round is unambiguously either a starting or an ending
round. Moreover, since $\operatorname{play}(\delta_{E},A_{E})$ moves are
always paired with $\operatorname{wait}(\delta_{C})$ ones, which are ending
moves, then $\operatorname{play}(\delta_{E},A_{E})$ moves are necessarily
ending moves (item 1 of Definition 3.2).

We can now specify how to apply a round to the current partial plan to obtain
the new one. The game always starts with a single starting round.

[Outcome of rounds] Let
${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ be an event
sequence, with ${\mu}_{n}=(A_{n},\delta_{n})$ (${\mu}_{n}=(\varnothing,0)$ if
${\overline{\mu}}=\varepsilon$). Let ${\rho}=({\mu}_{C},{\mu}_{E})$ be a
round, $A_{E}$ and $A_{C}$ be the sets of actions of the two moves ($A_{C}$ is
empty if ${\mu}_{C}$ is a $\operatorname{wait}$ move), and $\delta_{E}$ and
$\delta_{C}$ be the time increments of the moves. We define $\delta_{C}=1$
(resp., $\delta_{E}=1$) for $\operatorname{play}(A_{C})$ (resp.,
$\operatorname{play}(A_{E})$).

The _outcome_ of the application of ${\rho}$ on ${\overline{\mu}}$ is the
event sequence ${\rho}({\overline{\mu}})$ defined as follows:

  1. (1)

if ${\rho}$ is a starting round, then
${\rho}({\overline{\mu}})={\overline{\mu}}_{<n}{\mu}_{n}^{\prime}$, where
${\mu}_{n}^{\prime}\nobreak=\nobreak(A_{n}\cup A_{C}\cup A_{E},\delta_{n})$;

  2. (2)

if ${\rho}$ is an ending round, then
${\rho}({\overline{\mu}})={\overline{\mu}}{\mu}^{\prime}$, where
${\mu}^{\prime}=(A_{C}\cup A_{E},\delta_{E})$;

We say that ${\rho}$ is _applicable_ to ${\overline{\mu}}$ if:

  1. a)

${\rho}({\overline{\mu}})$ complies with Section 3.1;

  2. b)

${\rho}$ is an ending round if and only if ${\overline{\mu}}$ is open for all
variables that appear in the moves.

A single move by either player is applicable to ${\overline{\mu}}$ if there is
a move for the other player such that the resulting round is applicable to
${\overline{\mu}}$. The game starts from the empty partial plan $\varepsilon$,
and players play in turn, composing a round from the move of each one, which
is applied to the current partial plan to obtain the new one. We can now
define the notion of _strategy_ for each player and that of _winning strategy_
for _Charlie_.

[Strategy] A _strategy for Charlie_ is a function
${\sigma}_{C}:{\Pi}\to\mathcal{M}_{C}$ that maps any given partial plan
${\overline{\mu}}$ into a move ${\mu}_{C}$ applicable to ${\overline{\mu}}$. A
_strategy for Eve_ is a function
${\sigma}_{E}:{\Pi}\times\mathcal{M}_{C}\to\mathcal{M}_{E}$ that maps a
partial plan ${\overline{\mu}}$ and a move ${\mu}_{C}\in\mathcal{M}_{C}$
applicable to ${\overline{\mu}}$ into a move ${\mu}_{E}$ such that the round
${\rho}=({\mu}_{C},{\mu}_{E})$ is applicable to ${\overline{\mu}}$.

A sequence ${\overline{\rho}}=\langle{\rho}_{0},\ldots,{\rho}_{n}\rangle$ of
rounds is called a _play_ of the game. A play is said to be _played according
to_ some strategy ${\sigma}_{C}$ for _Charlie_ , if, starting from the initial
partial plan ${\overline{\mu}}_{0}=\varepsilon$, it holds that
${\rho}_{i}=({\sigma}_{C}(\Pi_{i-1}),{\mu}_{E}^{i})$, for some
${\mu}_{E}^{i}$, for all $0<i\leq n$, and to be played according to some
strategy ${\sigma}_{E}$ for _Eve_ if
${\rho}_{i}=({\mu}_{C}^{i},{\sigma}_{E}(\Pi_{i-1},{\mu}_{C}^{i}))$, for all
$0<i\leq n$. It can be easily seen that for any pair of strategies
$({\sigma}_{C},{\sigma}_{E})$ and any $n\geq 0$, there is a unique play
${\overline{\rho}}_{n}({\sigma}_{C},{\sigma}_{E})$ of length $n$ played
according to both ${\sigma}_{C}$ and ${\sigma}_{E}$.

Then, we say that a partial plan ${\overline{\mu}}$ and the play
${\overline{\rho}}$ such that
${\overline{\mu}}={\overline{\rho}}(\varepsilon)$ are _admissible_ , if the
partial plan satisfies the domain rules, and that they are _successful_ if the
partial plan satisfies the system rules.

[Admissible strategy for _Eve_ ] A strategy ${\sigma}_{E}$ for _Eve_ is
_admissible_ if for each strategy ${\sigma}_{C}$ for _Charlie_ , there is
$k\geq 0$ such that the play
${\overline{\rho}}_{k}({\sigma}_{C},{\sigma}_{E})$ is admissible.

_Charlie_ wins if, _assuming_ that domain rules are respected, he manages to
satisfy the system rules no matter how _Eve_ plays.

[Winning strategy for _Charlie_ ] Let ${\sigma}_{C}$ be a strategy for
_Charlie_. We say that ${\sigma}_{C}$ is a _winning strategy_ for _Charlie_ if
for any _admissible_ strategy ${\sigma}_{E}$ for _Eve_ , there exists $n\geq
0$ such that the play ${\overline{\rho}}_{n}({\sigma}_{C},{\sigma}_{E})$ is
successful.

We say that _Charlie_ _wins_ the game $G$ if he has a winning strategy, while
_Eve_ _wins_ the game if a winning strategy for _Charlie_ does not exist.

###  3.3. Synthesis

The synthesis problem is the problem of devising an implementation that
satisfies a formal specification of an input-output relation [PR89a]. Such an
implementation may be a transducer, a Mealy machine, a Moore machine, a
circuit, or the like. In the following, we give a short account of the roles
of games and strategies in game-based synthesis.

[Game Graph] A finite game graph $G$ is a triple $\left(Q,Q_{C},E\right)$,
where $Q$ is a finite set of nodes, $Q_{C}\subseteq Q$ is the subset of
_Charlie_ ’s nodes, and $E\subseteq Q\times Q$ is a transition relation. The
relation $E$ must satisfy the condition: $\forall q\exists
q^{\prime}:\left(q,q^{\prime}\right)\in E$ (totality).

A _play_ on a game graph $G$ starting from the initial state $q_{0}$ is an
infinite sequence $p=q_{0}q_{1}q_{2}\ldots$, where $(q_{i},q_{i+1})\in E$, for
all $i\geq 0$. A game is a pair $(G,\mathcal{W})$, where $G$ is a game graph
and $\mathcal{W}$ is the winning condition of the game. In the general case,
$\mathcal{W}$ consists of the set of plays won by _Charlie_.

Here, we focus on reachability winning conditions, which are expressed as
$\mathcal{W}\vcentcolon=\\{R\subseteq Q\mid R\cap F\neq\varnothing\\}$, for a
given set $F\subseteq Q$. A play $p$ is said to satisfy $\mathcal{W}$ if the
set of states visited by $p$, denoted by $occ(p)=\\{q\in Q\mid\exists
i\mathrel{.}p(i)=q\\}$, intersects $\mathcal{W}$, that is, _Charlie_ wins the
play $p$ if $p$ visits at least one state in $F$.

[Reachability game] A reachability game is a pair $(G,\mathcal{W})$, where
$G=(Q,Q_{C},E)$ is a game graph and $\mathcal{W}$ is a reachability winning
condition.

A strategy for _Charlie_ is a function $f:Q^{*}\cdot Q_{C}\rightarrow Q$. A
play $p$ adheres to strategy $f$ if, for each $q_{i}\in Q_{C}$,
$q_{i+1}=f(q_{0}\ldots q_{i})$. Given an initial state $q$, a strategy for
_Charlie_ is a winning strategy if _Charlie_ wins any play from $q$ that
follows the strategy $f$. The same holds for _Eve_. _Charlie_ (resp., _Eve_)
wins if a winning strategy exists from $q$.

Given a game $(G,\mathcal{W})$, with $G=(Q,Q_{C},E)$, the winning region of
_Charlie_ is defined as $W_{C}\vcentcolon=\\{q\in Q\,|\,\emph{Charlie}\text{
wins from q }\\}$. The winning region $W_{E}$ for _Eve_ is defined in an
analogous way. The two sets are clearly disjoint ($W_{C}\cap
W_{E}=\varnothing$). The game is said to be _determined_ if $W_{C}\cup
W_{E}=Q$. It is well known that reachability games are determined [Tho08].

The next step is to build a Controller starting from a winning strategy $f$
such that the specification is met. We use Moore machines as _Charlie_ plays
first.

[Moore machine] A Moore machine is a tuple
$M=(Q,\Sigma,\Gamma,q_{0},\delta,\tau)$, where $Q$ is a finite set of states,
$\Sigma$ is a finite input alphabet, $\Gamma$ is a finite output alphabet,
$q_{0}\in Q$ is the initial state, $\delta:Q\times\Sigma\rightarrow Q$ is the
transition function, and $\tau:Q\rightarrow\Gamma$ it the output function.

By suitably tying $\delta$ and $\tau$ to $f$, one can effectively implement
$f$. We refer the reader to 5.1 for the details on how we do it.

###  3.4. Difference Bound Matrices

_Difference bound matrices_ (DBMs) were introduced by Dill [Dil89] as a
pragmatic representation of constraints $(x-y\leq c)$. Later on, Péron et al.
[PH07] suitably expanded the formalism. The following short account of the
formalism is basically borrowed from the latter work,

Let $\mathit{Var}=\\{v_{0},v_{1},\ldots v_{n}\\}$ be a finite set of
variables, $\overline{V}=\mathbb{Z}\cup\\{+\infty\\}$ be a set of values that
variables and constants can take, and $C$ be a set of constraints of the form
$v_{i}-v_{j}\leq c$, where $v_{i},v_{j}\in\mathit{Var}$ and
$c\in\overline{V}$. The DBM that represents $C$ is an $(n+1)\times(n+1)$
matrix defined as follows:

$M_{ij}=\text{inf}\\{c\,\mid\,(v_{i}-v_{j}\leq c)\in C\\},$

where $\text{inf}(\varnothing)=+\infty$.

$M_{ij}$ equals the tightest value of $c$ if there is some constraint
$(v_{i}-v_{j}\leq c)$ in $C$; otherwise, it is $+\infty$. The variable
$v_{0}\in\mathit{Var}$ is always valued to $0$, and it is used to express
bounds on variables, that is, $v_{i}\leq c$ is written as $v_{i}-v_{0}\leq c$.
In Section 4, we use DBMs to conveniently represent atoms (see Section 3.1).

##  4\. A deterministic automaton for timeline-based planning

In this section, we define an encoding of timeline-based planning problems
into _deterministic_ finite state automata (DFA). Given a timeline-based
planning problem, the corresponding automaton recognizes all and only those
_event sequences_ that represent solution plans for the problem. In the next
section, we will use such an automaton as the game arena for a timeline-based
game.

###  4.1. Plans as words

Let $P=(\mathsf{SV},S)$ be a timeline-based planning problem and, as already
stated in the previous section, let $d=\max(L,U)+1$, where $L$ and $U$ are the
maximum lower and (finite) upper bounds appearing in any rule of $P$. We
restrict our attention to event sequences where the distance between two
consecutive events is at most $d$. Such a restriction guarantees us the
finiteness of the considered alphabet, and it does not cause any loss in
generality, as proved by Lemma 4.8 of [Gig19]. Moreover, it agrees with the
notion of move of a timeline-based game (see Section 3.2).

We define the symbols of the alphabet $\Sigma$ as _events_ of the form
${\mu}=(A,\delta)$, where $A\subseteq\mathsf{A}_{\mathsf{SV}}$ and
$1\leq\delta\leq d$. Formally, $\Sigma=2^{\mathsf{A}_{\mathsf{SV}}}\times[d]$,
where $[d]=\\{1,\ldots,d\\}$. Note that the size of $\Sigma$ is exponential in
the size of the problem. Moreover, we define $\operatorname{window}(P)$ as the
sum of all the coefficients appearing as upper bounds in the rules of $P$.
This value represents the maximum amount of time a rule can “count” far away
from the occurrence of the quantified tokens. Consider, for instance, the
following rule:

$\displaystyle a_{0}[x_{0}=v_{0}]\to{}$ $\displaystyle\exists
a_{1}[x_{1}=v_{1}]a_{2}[x_{2}=v_{2}]a_{3}[x_{3}=v_{3}]\mathrel{.}$ (3)
$\displaystyle\operatorname{start}(a_{1})\mathrel{\mathsf{\leq}}_{[4,14]}\operatorname{end}(a_{0})\land\operatorname{end}(a_{0})\mathrel{\mathsf{\leq}}_{[0,+\infty]}\operatorname{end}(a_{2})\land\operatorname{start}(a_{2})\mathrel{\mathsf{\leq}}_{[0,3]}\operatorname{end}(a_{3})$

In this case, assuming the above rule to be the only one in the problem,
$\operatorname{window}(P)$ would be $3+14=17$. Thus, the rule can account for
what happens at most $17$ time points from the occurrence of its quantified
tokens. For instance, if the token $a_{1}$ appears at a specific distance from
$a_{0}$, it has to be within less than $17$ time points, and any modification
of the plan that alters this distance can break the rule’s satisfaction.
However, what occurs further away from $a_{0}$ only affects the fulfillment of
the rule _qualitatively_. Suppose that the tokens $a_{2}$ and $a_{3}$ are,
together, at $100$ time points from $a_{0}$. Changing this distance while
maintaining the qualitative order between tokens does not break the rule’s
satisfaction. For $\operatorname{window}(P)$’s properties refer to [Gig19].

###  4.2. Matching structures

A key insight underlying the construction we are going to outline is that
every atomic temporal relation $T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$
can be rewritten as the conjunction of two upper bound constraints
$T^{\prime}-T\leq u$ and $T-T^{\prime}\leq-l$, where we represent a lower
bound constraint $T^{\prime}-T\geq l$ as an upper bound one. This allows us to
rewrite the clause $\mathsf{C}$ of an existential statement $\mathsf{E}$ as a
constraint system $\nu(\mathsf{C})$ with constraints of the form
$T-T^{\prime}\leq n$, for $n\in\mathbb{Z}\cup\\{+\infty\\}$.

The constraint system $\nu(\mathsf{C})$ can be represented by a difference
bound matrix $D$ indexed by terms, where the entry $D[T,T^{\prime}]$ gives the
upper bound $n$ on $T-T^{\prime}$. In building $D$, we ensure the right
duration of tokens by augmenting the system with constraints of the kind
$\operatorname{start}(a_{i})-\operatorname{end}(a_{i})\leq-d^{x_{i}=v_{i}}_{min}$
and $\operatorname{end}(a_{i})-\operatorname{start}(a_{i})\leq
d^{x_{i}=v_{i}}_{max\vphantom{i}}$, for any quantified token
$a_{i}[x_{i}=v_{i}]$ of $\mathsf{E}$. As an example, the constraint system and
the DBM for the above rule are the ones in Figs. 1 and 2, respectively.

$\displaystyle\begin{cases}\operatorname{end}(a_{0})-\operatorname{start}(a_{1})&\leq
14\\\ \operatorname{start}(a_{1})-\operatorname{end}(a_{0})&\leq-4\\\
\operatorname{end}(a_{0})-\operatorname{end}(a_{2})&\leq 0\\\
\operatorname{end}(a_{3})-\operatorname{start}(a_{2})&\leq 3\\\
\operatorname{start}(a_{2})-\operatorname{end}(a_{3})&\leq 0\end{cases}$
Figure 1. The constraint system of Eq. 3.
$\begin{array}[]{rcccccccc}\hline\cr\hline\cr&\operatorname{start}(a_{0})&\operatorname{end}(a_{0})&\operatorname{start}(a_{1})&\operatorname{end}(a_{1})&\operatorname{start}(a_{2})&\operatorname{end}(a_{2})&\operatorname{start}(a_{3})&\operatorname{end}(a_{3})\\\
\hline\cr\operatorname{start}(a_{0})\\\ \operatorname{end}(a_{0})&&&14&&&0\\\
\operatorname{start}(a_{1})&&-4\\\ \operatorname{end}(a_{1})\\\
\operatorname{start}(a_{2})&&&&&&&&0\\\ \operatorname{end}(a_{2})&&&\\\
\operatorname{start}(a_{3})\\\ \operatorname{end}(a_{3})&&&&&3&&&\\\
\hline\cr\hline\cr\end{array}$ Figure 2. DBM of Eq. 3. Missing entries are
intended to be $+\infty$.

On top of DBMs, we define the concept of _matching structure_ , a data
structure that allows us to monitor and update the fulfillment of atomic
temporal relations among terms throughout the execution of the plan. More
precisely, it allows us to manipulate and reason about existential statements
of which only a portion of the requests has been satisfied by the word read so
far, while the rest is potentially satisfiable in the future.

[Matching Structure] Let $\mathsf{E}\equiv\exists a_{1}[x_{1}=v_{1}]\dots
a_{m}[x_{m}=v_{m}]\,.\,\mathsf{C}$ be an existential statement of a
synchronization rule $\mathsf{R}\equiv
a_{0}[x_{0}=v_{0}]\rightarrow\mathsf{E}_{1}\lor\dots\lor\mathsf{E}_{k}$ over
the set of state variables $\mathsf{SV}$. The _matching structure_ for
$\mathsf{E}$ is a tuple $\mathsf{M}_{\mathsf{E}}=(V,D,M,t)$, where:

  * •

$V$ is the set of terms $\operatorname{start}(a)$ and $\operatorname{end}(a)$,
for $a\in\\{a_{0},\dots,a_{m}\\}$;

  * •

$D$ is a DBM of size $|V|\times|V|$, indexed by terms of $V$, whose entries
take value over $\mathbb{Z}\cup\\{+\infty\\}$, where

$\displaystyle\begin{cases}D[T,T^{\prime}]=n&\quad if\;T-T^{\prime}\leq n\
\in\nu(\mathsf{C}),\\\ D[T,T^{\prime}]=0&\quad if\;T=T^{\prime},\\\
D[T,T^{\prime}]=+\infty&\quad otherwise;\end{cases}$

  * •

$M\subseteq V$ and $0\leq t\leq\operatorname{window}(P)$.

The set $M$ contains the set of terms from $V$ correctly seen in the sequence
so far. We say these terms have been _matched_ by the matching structure. We
use $\overline{M}=V\setminus M$ to refer to terms yet to be matched. We say a
matching structure $\mathsf{M}$ to be _closed_ if $M=V$, _initial_ if
$M=\varnothing$, and _active_ if $\operatorname{start}(a_{0})\in M$ and it is
not closed. The component $t$ represents the time elapsed since matching
$\operatorname{start}(a_{0})$. As time progresses, we update a matching
structure as follows.

In the DBMs of a matching structure, the bounds between any pair of terms $T$
and $T^{\prime}$, with one in $M$ while the other not, are tightened by the
elapsing of time. When $T\in M$ and $T^{\prime}\in\overline{M}$,
$D[T,T^{\prime}]$ is a lower bound loosened by adding the elapsed time
$\delta$. When $T\in\overline{M}$ and $T^{\prime}\in M$, $D[T,T^{\prime}]$ is
an upper bound tightened by subtracting $\delta$. Consider the DBM in Figure 2
and the pair of terms $\operatorname{start}(a_{1})$ and
$\operatorname{end}(a_{0})$. We have
$D[\operatorname{start}(a_{1}),\operatorname{end}(a_{0})]=-4$, implying that
$\operatorname{start}(a_{1})-\operatorname{end}(a_{0})\leq-4$ must hold.
Suppose that $\operatorname{start}(a_{1})\in M$ (it has been matched), and
that $\operatorname{end}(a_{0})\in\overline{M}$ (it needs to be matched). Now,
in a time step, the entry in the DBM is incremented and updated to $-4+1=-3$
reflecting the fact that we now have $3$ time steps left to match
$\operatorname{end}(a_{0})$. A similar analysis leads us to the conclusion
that the entry $D[\operatorname{end}(a_{0}),\operatorname{start}(a_{1})]=14$
has to be decremented by $1$ and updated to $14-1=13$. This intuition is
formalized as follows.

[Time shifting] Let $\delta>0$ be a positive amount of time, and let
$\mathsf{M}=(V,D,M,t)$ be a matching structure. The result of shifting
$\mathsf{M}$ by $\delta$ time units, written $\mathsf{M}+\delta$, is a
matching structure $\mathsf{M}^{\prime}=(V,D^{\prime},M,t^{\prime})$, where:

  * •

for all $T,T^{\prime}\in V$:

$D^{\prime}[T,T^{\prime}]=\begin{cases}D[T,T^{\prime}]+\delta&\text{if }T\in
M\text{ and }T^{\prime}\in\overline{M}\\\ D[T,T^{\prime}]-\delta&\text{if
}T\in\overline{M}\text{ and }T^{\prime}\in M\\\
D[T,T^{\prime}]&\text{otherwise}\end{cases}$

  * •

and

$t^{\prime}=\begin{cases}t+\delta&\text{if }\mathsf{M}\text{ is
\emph{active}}\\\ t&\text{otherwise}\end{cases}$

Figure 2 specifies how to update the entries of $D$ and how to update $t$ to
the trigger occurrence of an active matching structure.

[Matching] Let $\mathsf{M}=(V,D,M,t)$ be a matching structure and
$I\subseteq\overline{M}$ a set of matched terms. A matching structure
$\mathsf{M}^{\prime}=(V,D,M^{\prime},t)$ is the result of matching the set
$I$, written $\mathsf{M}\cup I$, with $M^{\prime}=M\cup I$.

To correctly match an existential statement while reading an event sequence, a
matching structure is updated only as long as one witnesses no violation of
temporal constraints. As such, we deem an event as _admissible_ or not.

[Admissible Event] An event ${\mu}=(A,\delta)$ is _admissible_ for a matching
structure $\mathsf{M}_{\mathsf{E}}=(V,D,M,t)$ if and only if, for every $T\in
M$ and $T^{\prime}\in\overline{M}$, $\delta\leq D[T^{\prime},T]$, the elapsing
of $\delta$ time units does not exceed the upper bound of some term
$T^{\prime}$ not yet matched by $\mathsf{M}_{\mathsf{E}}$.

Each admissible event ${\mu}$ that is read can be matched with a subset of
terms from the matching structure. However, there can be multiple ways to
match events and terms. To make this choice explicit, we introduce the
following definition.

[$I$-match Event]Let $\mathsf{M}_{\mathsf{E}}=(V,D,M,t)$ be a matching
structure and $I\subseteq\overline{M}$. An $I$_-match event_ is an admissible
event ${\mu}=(A,\delta)$ for $\mathsf{M}_{\mathsf{E}}$ such that:

  1. (1)

for all token names $a\in\mathsf{N}$ quantified as $a[x=v]$ in $\mathsf{E}$ we
have that:

    1. (a)

if $\operatorname{start}(a)\in I$, then $\operatorname{start}(x,v)\in A$;

    2. (b)

$\operatorname{end}(a)\in I$ if and only if $\operatorname{start}(a)\in M$ and
$\operatorname{end}(x,v)\in A$;

  2. (2)

and for all $T\in I$ it holds that:

    1. (a)

for every other term $T^{\prime}\in V$, if $D[T^{\prime},T]\leq 0$, then
$T^{\prime}\in M\cup I$;

    2. (b)

for all $T^{\prime}\in M$, $\delta\geq-D[T^{\prime},T]$, all the lower bounds
on $T$ are satisfied;

    3. (c)

for each other term $T^{\prime}\in I$, either $D[T^{\prime},T]=0$,
$D[T,T^{\prime}]=0$, or $D[T^{\prime},T]=D[T,T^{\prime}]=+\infty$.

We consider an event ${\mu}$ an $I$-match event if its actions correspond to
the terms in $I$. The definition in Item 1 ensures the correct matching of
each term to an action it represents and that the endpoints of a quantified
token precisely identify the endpoints of a token in the event sequence.
Meanwhile, Item 2 guarantees that matching the terms in $I$ does not violate
any atomic temporal relation. In addition, Item 2a deals with the qualitative
aspect of a “happens before” relation, while Items 2b and 2c address the
quantitative aspects of the lower bounds of these relations. It is worth
noting that an $\varnothing$-event is also considered admissible.

Let $\mathbb{M}_{P}$ denote the set of all matching structures for a planning
problem $P$, and let $\mathbb{I}$ be the set of all possible terms built from
token names in $\mathsf{N}$. To describe the evolution of a matching
structure, we define a quaternary relation
$S\subseteq\mathbb{M}_{P}\times\Sigma\times\mathbb{I}\times\mathbb{M}_{P}$ as
$(\mathsf{M},{\mu},I,\mathsf{M}^{\prime})\in{S}$, for an event
${\mu}=(A,\delta)$, if and only if ${\mu}$ is an $I$-match event for
$\mathsf{M}$, and $\mathsf{M}^{\prime}=(\mathsf{M}+\delta)\cup I$. We also
write $\mathsf{M}\mathrel{\xlongrightarrow{{\mu},{I}}}\mathsf{M}^{\prime}$ in
place of $(\mathsf{M},{\mu},I,\mathsf{M}^{\prime})\in{S}$. Note that, from
Figure 2, a single event can represent multiple $I$-match events for a
matching structure. Therefore, given a matching structure $\mathsf{M}$ and an
event ${\mu}$, automaton states will collect all the matching structures
$\mathsf{M}^{\prime}$ resulting from the relation $S$, for some set of terms
$I$. Given a set of matching structures $\Upsilon$, this notion is best
described by the function
$\operatorname{step}_{\mu}(\Upsilon)=\\{\mathsf{M}^{\prime}\mid(\mathsf{M},{\mu},I,\mathsf{M}^{\prime})\in
S,\text{ for some }\mathsf{M}\in\Upsilon\text{ and }I\in\mathbb{I}\\}$.
Furthermore, we define $\Upsilon^{\mathsf{R}}_{t}\subseteq\Upsilon$ as the set
of all the _active_ matching structures $\mathsf{M}\in\Upsilon$ with timestamp
$t$, associated with any existential statement of $\mathsf{R}$. Matching
structures in $\Upsilon^{\mathsf{R}}_{t}$ contribute to fulfilling the same
triggering event of $\mathsf{R}$, regardless of their existential statement.
We also define $\Upsilon_{\bot}\subseteq\Upsilon$ as the set of _non-active_
matching structures of $\Upsilon$. Lastly, we say that $\Upsilon$ is _closed_
if there exists $\mathsf{M}\in\Upsilon$ such that $\mathsf{M}$ is _closed_.

$x_{0}$ $x_{0}=v_{0}$gT $x_{0}=v^{\prime}_{0}$gT$x_{1}$
$x_{1}=v^{\prime}_{1}$gT $x_{1}=v_{1}$gT
$x_{1}=v^{{}^{\prime\prime}}_{1}$gT$x_{2}$ $x_{2}=v^{\prime}_{2}$gT
$x_{2}=v_{2}$gT $x_{2}=v^{{}^{\prime\prime}}_{2}$gT$x_{3}$ $x_{3}=v_{3}$gT
$x_{3}=v^{\prime}_{3}$gT Figure 3. Example of timelines for variables
$x_{0},\,x_{1},\,x_{2},\,x_{3}$.

We conclude this section by providing an example of updating a matching
structure $\mathsf{M}=(V,D,M,t)$ for the rule discussed at the beginning of
the section. Consider the set of timelines in Fig. 3. Before matching any term
$\mathsf{M}$ is initial with $M=\varnothing$, $t=0$, $D$ as the DBM in Fig. 2,
and $V$ as the set of term $\operatorname{start}(a)$ and
$\operatorname{end}(a)$ for $a\in\\{a_{0},a_{1},a_{2},a_{3}\\}$. We begin by
matching the terms $\operatorname{start}(a_{0})$ and
$\operatorname{start}(a_{3})$ from the event
${\mu}=(\\{\operatorname{start}(x_{0},v_{0}),\operatorname{start}(x_{3},v_{3})\\},0)$
(we do not consider $\operatorname{start}(x_{1},v^{\prime}_{1})$ and
$\operatorname{start}(x_{2},v^{\prime}_{2})$ since they are not in $V$). Such
event is an $I$-match event for
$I=\\{\operatorname{start}(a_{0}),\operatorname{start}(a_{3})\\}$: it is an
admissible event (Fig. 2), Item 1a holds, for both
$\operatorname{start}(a_{0})$ and $\operatorname{start}(a_{3})$, there are no
terms that should appear before them (Item 2a), there are no related lower
bounds (Item 2b), and
$D[\operatorname{start}(a_{0}),\operatorname{start}(a_{3})]=D[\operatorname{start}(a_{3}),\operatorname{start}(a_{0})]=+\infty$
(Item 2c). Hence, we update $M=M\cup
I=\\{\operatorname{start}(a_{0}),\operatorname{start}(a_{3})\\}$ and
$t=t+\delta=0$; now $\mathsf{M}$ is active. The next term to consider is
$\operatorname{start}(a_{2})$, which occurs after $\delta=5$ time steps.

First, we ensure that the event ${\mu}=(\operatorname{start}(x_{2},v_{2}),5)$
is admissible. We show that by examining the DBM in Fig. 2, we see that the
elapsing of time $\delta$ does not exceed any upper bound related to terms
$T\in M$ and $T^{\prime}\in\overline{M}$. Next, the set $I$ in the current
state appears as $I=\\{\operatorname{start}(a_{2})\\}$. Notice that we are in
the case of Item 1a, and Item 2 holds because no constraint involves the term
$\operatorname{start}(a_{2})$ (Item 2a), no lower bounds are related to
$\operatorname{start}(a_{2})$ (Item 2b), and $\operatorname{start}(a_{2})$ is
the only term in $I$ (Item 2c). Therefore, from Figs. 2 and 2, we update
$\mathsf{M}$ as follows: $\mathsf{M}=(\mathsf{M}+\delta)\cup I$. Each entry of
the DBM will remain unchanged since the third update case of Fig. 2 applies,
$M=M\cup
I=\\{\operatorname{start}(a_{0}),\operatorname{start}(a_{3}),\operatorname{start}(a_{2})\\}$,
and $t=t+\delta=5$.

Similarly, for the next event is
${\mu}=(\operatorname{start}(x_{1},v_{1}),1)$, we check if such an event is
admissible, and indeed it is since the upper bound
$D[\operatorname{end}(a_{0}),\operatorname{start}(a_{1})]=9\geq\delta$. It is
also an $I$-match event for $I=\\{\operatorname{start}(a_{1})\\}$, since it
respects Item 1a and all the relations in Item 2; thus we update $\mathsf{M}$.
We decrement $D[\operatorname{end}(a_{3}),\operatorname{start}(a_{2})]$ and
increment $D[\operatorname{start}(a_{2}),\operatorname{end}(a_{3})]$ by 1 (see
Fig. 2), update $M$ like follows
$M=\\{\operatorname{start}(a_{0}),\operatorname{start}(a_{3}),\operatorname{start}(a_{2}),\operatorname{start}(a_{1})\\}$,
and $t=t+\delta=5+1=6$.

The next event is ${\mu}=(\operatorname{end}(x_{3},v_{3}),3)$ after 2 time
steps. Note that it is an admissible event and also an $I$-match event for
$I=\\{\operatorname{end}(a_{3})\\}$. In this case, we emphasize that Items 1b
and 2 are respected. We update the DBM as follows:
$D[\operatorname{end}(a_{0}),\operatorname{start}(a_{1})]=14-2=12$,
$D[\operatorname{start}(a_{1}),\operatorname{end}(a_{0})]=-4+2=-2$,
$D[\operatorname{end}(a_{3}),\operatorname{start}(a_{2})]=2-2=0$,
$D[\operatorname{start}(a_{2}),\operatorname{end}(a_{3})]=1+2=3$. Then, we
update $M=M\cup
I=\\{\operatorname{start}(a_{0}),\operatorname{start}(a_{3}),\operatorname{start}(a_{2}),\\\
\operatorname{start}(a_{1}),\operatorname{end}(a_{3})\\}$ and
$t=t+\delta=6+2=8$. Notice that if we did not match
$\operatorname{end}(a_{3})$ now, at the next time step, the timeline would
have violated the rule above because the upper bound
$D[\operatorname{end}(a_{3}),\operatorname{start}(a_{2})]=0$.

The subsequent event is
${\mu}=(\operatorname{end}(x_{1},v_{1}),\operatorname{start}(x_{1}=v^{\prime}_{1}),6)$
for which $I=\operatorname{end}(a_{1})$. Since there is no constraint
involving $\operatorname{end}(a_{1})$, this event is admissible and an
$I$-match event. The DBM is shifted by 6 time steps, and
$M=\\{\operatorname{start}(a_{0}),\operatorname{start}(a_{3}),\operatorname{start}(a_{2}),\operatorname{start}(a_{1}),\operatorname{end}(a_{1})\\}$.

The last event
${\mu}=(\\{\operatorname{start}(x_{0},v^{\prime}_{0}),\operatorname{start}(x_{2},v^{{}^{\prime\prime}}_{2}),\operatorname{end}(x_{0},v_{0}),\operatorname{end}(x_{2},v_{2})\\},2)$
is admissible and an $I$-match for
$I=\\{\operatorname{end}(a_{0}),\operatorname{end}(a_{2})\\}$, note that there
is not an upper bound between $\operatorname{end}(a_{0})$ and
$\operatorname{end}(a_{2})$ and that Items 1b and 2 of the definition of
$I$-match event are respected.

###  4.3. Building the automaton

We can now define the automaton. First, given an existential statement
$\mathsf{E}$, let $\mathbb{E}_{\mathsf{E}}$ be the set of all existential
statements in the same rule of $\mathsf{E}$. Next, let $\mathbb{F}_{P}$ be the
set of functions that map each existential statement of $P$ to a set of
existential statements and let $\mathbb{D}_{P}$ be the set of functions that
map each existential statement to a set of matching structures $\Upsilon$. An
automaton $\mathsf{T}_{P}$ that checks the transition functions of the
variables is easy to define. Then, given a timeline-based planning problem
$P=(\mathsf{SV},S)$, we can characterize the corresponding automaton as
$A_{P}=\mathsf{T}_{P}\cap\mathsf{S}_{P}$. Here, $\mathsf{S}_{P}$ checks the
fulfillment of the synchronization rules, and we define it as
$\mathsf{S}_{P}=(Q,\Sigma,q_{0},F,\tau)$ where

  1. (1)

$Q=2^{\mathbb{M}_{P}}\times\mathbb{D}_{P}\times\mathbb{F}_{P}\cup\\{\bot\\}$
is the finite set of states, states are tuples of the form
$\langle\Upsilon,\Delta,\Phi\rangle\in
2^{\mathbb{M}_{P}}\times\mathbb{D}_{P}\times\mathbb{F}_{P}$, plus a sink state
$\bot$;

  2. (2)

$\Sigma$ is the input alphabet defined above;

  3. (3)

the initial state $q_{0}=\langle\Upsilon_{0},\Delta_{0},\Phi_{0}\rangle$ is
such that $\Upsilon_{0}$ is the set of initial matching structures of the
existential statements of $P$ and, for all existential statements $\mathsf{E}$
of $P$, we have $\Delta_{0}(\mathsf{E})=\varnothing$ and
$\Phi_{0}(\mathsf{E})=\mathbb{E}_{\mathsf{E}}$;

  4. (4)

$F\subseteq Q$ is the set of final states defined as:

$F=\Set{\langle\Upsilon,\Delta,\Phi\rangle\in
Q}{\begin{gathered}\mathsf{M}\text{ is not \emph{active} for all
}\mathsf{M}\in\Upsilon\\\ \text{and }\Delta(\mathsf{E})=\varnothing\text{ for
all }\mathsf{E}\text{ of }P\end{gathered}}$

  5. (5)

$\tau:Q\times\Sigma\rightarrow Q$ is the transition function that given a
state $q=\langle\Upsilon,\Delta,\Phi\rangle$ and a symbol ${\mu}=(A,\delta)$
computes the new state $\tau(q,{\mu})$. Let
$\operatorname{step}^{\mathsf{E}}_{\mu}(\Upsilon^{\mathsf{R}}_{t})=\\{\mathsf{M}_{\mathsf{E}}\mid\mathsf{M}_{\mathsf{E}}\in\operatorname{step}_{\mu}(\Upsilon^{\mathsf{R}}_{t})\\}$.
Moreover, let
$\Psi^{\mathsf{R}}_{t}=\\{\mathsf{E}|\mathsf{M}_{\mathsf{E}}\in\operatorname{step}_{\mu}(\Upsilon^{\mathsf{R}}_{t})\\}$.
Then, the updated components of the state are based on what follows, where
$W=\operatorname{window}(P)$:

$\displaystyle\Upsilon^{\prime}$
$\displaystyle=\operatorname{step}_{\mu}(\Upsilon_{\bot})\cup\bigcup\Set{\operatorname{step}_{\mu}(\Upsilon^{\mathsf{R}}_{t})}{\text{$t\leq
W-\delta$ and $\operatorname{step}_{\mu}(\Upsilon^{\mathsf{R}}_{t})$ is not
\emph{closed}}}$ $\displaystyle\Delta^{\prime}(\mathsf{E})$
$\displaystyle=\begin{cases}\operatorname{step}^{\mathsf{E}}_{\mu}(\Upsilon^{\mathsf{R}}_{t})&\text{where
$t$ is the minimum such that $t>W-\delta$ and
$\operatorname{step}^{\mathsf{E}}_{\mu}(\Upsilon^{\mathsf{R}}_{t})\neq\varnothing$}\\\
\operatorname{step}_{\mu}(\Delta(\mathsf{E}))&\text{if such $t$ does not
exist}\end{cases}$ $\displaystyle\Phi^{\prime}(\mathsf{E})$
$\displaystyle=\begin{cases}\mathbb{E}_{\mathsf{E}}\quad\text{if
$\mathsf{E}\in\Psi(\mathsf{E}^{\prime})$ for some $\mathsf{E}^{\prime}$ such
that $\Delta^{\prime}(\mathsf{E}^{\prime})$ is \emph{closed}}\\\
\Phi(\mathsf{E})\setminus\\{\mathsf{E}^{\prime}\mid\exists
t>W-\delta\mathrel{.}\mathsf{E}^{\prime}\in\Psi^{\mathsf{R}}_{t}\land\mathsf{E}\not\in\Psi^{\mathsf{R}}_{t}\\}\quad\text{otherwise}\end{cases}$

Let $\Delta^{\prime\prime}(\mathsf{E})=\Delta^{\prime}(\mathsf{E})$ unless
there is an $\mathsf{E}^{\prime}$ with
$\mathsf{E}\in\Phi^{\prime}(\mathsf{E}^{\prime})$ such that
$\Delta^{\prime}(\mathsf{E}^{\prime})$ is _closed_ , in which case
$\Delta^{\prime\prime}(\mathsf{E})=\varnothing$. Then,
$\tau(q,{\mu})=\langle\Upsilon^{\prime},\Delta^{\prime\prime},\Phi^{\prime}\rangle$
if the following holds:

    1. (a)

for every $\Upsilon^{\mathsf{R}}_{t}$,
$\operatorname{step}_{\mu}(\Upsilon^{\mathsf{R}}_{t})\neq\varnothing$, and

    2. (b)

for every synchronization rule $\mathsf{R}\equiv
a_{0}[x_{0}=v_{0}]\rightarrow\mathsf{E}_{1}\lor\dots\lor\mathsf{E}_{n}$ in
$S$, if $\operatorname{start}(x_{0},v_{0})\in A$, then there exists
$\mathsf{M}_{\mathsf{E}_{i}}=(V,D,M,0)\in\Upsilon^{\prime}$, with
$i\in\\{1\dots n\\}$, such that $\operatorname{start}(a_{0})\in M$;

Otherwise, $\tau(q,{\mu})=\bot$.

The first component $\Upsilon$ of an automaton’s state $q$ is a set of
matching structures that keeps track of the occurred events in the last
$\operatorname{window}(P)$ time points. The timestamp $t$ of any matching
structure in $\Upsilon$ satisfies $t<\operatorname{window}(P)$. These matching
structures evolve using the $\operatorname{step}_{\mu}$ function until they
become closed or their timestamp reaches $\operatorname{window}(P)$.

Matching structures that reach $\operatorname{window}(P)$ get promoted to a
new role where they record the pieces of existential statements not yet
matched to satisfy all the trigger events of $\mathsf{R}$ that occurred before
the last $\operatorname{window}(P)$ time points. However, the automaton does
not store these matching structures in $\Upsilon$. Instead, it uses the
function $\Delta$ mapping each existential statement $\mathsf{E}$ of a rule
$\mathsf{R}$ to the set of matching structures for $\mathsf{E}$ with
$t=\operatorname{window}(P)$. Thus, effectively summarizing events happening
before this window to keep size under control.

When a set $\Upsilon^{\mathsf{R}}_{t}$ exceeds the bound
$\operatorname{window}(P)$, the $\Delta$ function needs to be updated by
merging the information from $\Upsilon^{\mathsf{R}}_{t}$ with the information
already stored in $\Delta$. However, closing a set $\Delta(\mathsf{E})$ does
not necessarily mean that every event that triggered $\mathsf{R}$ satisfies
$\mathsf{R}$. This is because there may be other sets, say
$\Delta(\mathsf{E}^{\prime})$, responsible for fulfilling the same rule
$\mathsf{R}$, but for different trigger events. Therefore, closing
$\Delta(\mathsf{E})$ alone does not imply that $\mathsf{R}$ has been
satisfied. Conversely, there may be cases where $\Delta(\mathsf{E})$ and
$\Delta(\mathsf{E}^{\prime})$ contribute to match the same trigger events, and
closing either set is enough to satisfy $\mathsf{R}$.

To address the issue of lost information when adding a set of matching
structures to $\Delta$, we introduce the $\Phi$ function, mapping existential
statements to sets of existential statements, as the third component of the
automaton states. For an existential statement $\mathsf{E}$ and for every
existential statement $\mathsf{E}^{\prime}\in\Phi(\mathsf{E})$, it holds that
the set of matching structures $\Delta(\mathsf{E}^{\prime})$ tracks the
satisfaction of the same trigger events as the set $\Delta(\mathsf{E})$. This
way, when a set $\Delta(\mathsf{E})$ is closed, we can discard its matching
structures as well as the matching structures in
$\Delta(\mathsf{E}^{\prime})$.

In Section 4.4 we state and prove soundness and completeness of the automaton
construction. Now, instead, let us address the size of the automaton.

Let us recall that we assumed that the timestamp of each event in an event
sequence is bounded. However, it is worth noting that since events may have an
empty set of actions, Theorem 5 can handle arbitrary event sequences as well,
provided that we add suitable empty events. Let us now analyze the size of the
automaton.

######  Theorem 1 (Size of the automaton).

Let $P=(\mathsf{SV},S)$ be a timeline-based planning problem and let
$\mathsf{A}_{P}$ be the associated automaton. Then, the size of $A_{P}$ is at
most doubly-exponential in the size of $P$.

######  Proof 4.1.

We define $E$ as the overall number of existential statements in $P$, which is
linear in the size of $P$. We can then observe that
$|\mathbb{D}_{P}|\in\mathop{\mathcal{O}}({(2^{|\mathbb{M}_{P}|})}^{E})=\mathop{\mathcal{O}}(2^{E\cdot|\mathbb{M}_{P}|})$,
thus the number of $\Delta$ functions is doubly exponential in the size of
$P$. Next, note that
$\lvert\mathbb{F}_{P}\rvert\in\mathcal{O}({(2^{E})}^{E})=\mathcal{O}(2^{E^{2}})$.
Then, $|\mathsf{S}_{P}|\in\mathop{\mathcal{O}}(|\Sigma|\cdot
2^{|\mathbb{M}_{P}|})$ indicating that the size of $\mathsf{S}_{P}$ is at most
exponential in the number of possible matching structures. To bound this
number, we define $N$ as the largest finite constant appearing in $P$ in any
atom or value duration and $L$ as the length of the longest existential prefix
of an existential statement occurring inside a rule of $P$. Note that $N$ is
exponential in the size of $P$ since constants are expressed in binary, while
$L\in\mathop{\mathcal{O}}(|P|)$. We can then observe that the entries of a DBM
for $P$, of which the number is quadratic in $L$, are constrained to take
values within the interval $[-N,N]$ (excluding the value $+\infty$), which
size is linear in $N$. By Figure 2, it follows that
$|\mathbb{M}_{P}|\in\mathop{\mathcal{O}}(N^{L^{2}}\cdot
2^{L}\cdot\operatorname{window}(P))$ indicating that the number of matching
structures is at most exponential in the size of $P$.

Note that our automaton is the same size as the automaton built by Della
Monica et al. in [DGMS18]. However, while their automaton is nondeterministic,
ours is deterministic: an essential property to achieve the
$\mathsf{2EXPTIME}$ optimal asymptotic complexity for the synthesis procedure.

###  4.4. Soundness and Completeness

In the following, we present auxiliary notation, definitions, and essential
lemmas for establishing the soundness and completeness of the automaton
construction. For readability, we have included proofs in the appendix.

[Run of a matching structure] Let
${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ be a (possibly
open) event sequence, and let $\mathsf{M}_{\mathsf{E}}$ be the initial
matching structure of an existential statement $\mathsf{E}$. A _run_ of
$\mathsf{M}_{\mathsf{E}}$ on ${\overline{\mu}}$ yielding a matching structure
$\mathsf{M}_{n}$ is a sequence
${\overline{}{I}}=\langle{I}_{1},\ldots,{I}_{n}\rangle$ of $I$-match events
for the matching structures
$\langle\mathsf{M}_{\mathsf{E}},\mathsf{M}_{1},\ldots,\mathsf{M}_{n-1}\rangle$,
such that for every $i\in[1,\ldots,n]$,
$\mathsf{M}_{i-1}\mathrel{\xlongrightarrow{{\mu}_{i},{I}_{i}}}\mathsf{M}_{i}$.
We write
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},{\overline{}{I}}}\mathsf{M}_{n}$
when such run exists, or
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}}}\mathsf{M}_{n}$, if
${\overline{}{I}}$ is not relevant.

To link matching structures with the semantics of synchronization rules we
establish a connection between matching functions (Section 3.1) and runs.

######  Lemma 2 (Correspondence between runs and matching functions).

Let ${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ be a (possibly
open) event sequence, and let $\mathsf{M}_{\mathsf{E}}$ be the initial
matching structure of an existential statement $\mathsf{E}\equiv\exists
a_{1}[x_{1}=v_{1}]\ldots a_{k}[x_{k}=v_{k}]\mathrel{.}\mathsf{C}$, with
$\mathsf{C}$ augmented with atoms
$\operatorname{start}(a_{i})\mathrel{\mathsf{\leq}}_{[d^{x_{i}=v_{i}}_{min},d^{x_{i}=v_{i}}_{max\vphantom{i}}]}\operatorname{end}(a_{i})$,
for every $0\leq i\leq k$. Then, there exists a run
${\overline{}{I}}=\langle{I}_{1},\ldots,{I}_{n}\rangle$ of
$\mathsf{M}_{\mathsf{E}}$ on ${\overline{\mu}}$, yielding a matching structure
$\mathsf{M}_{n}=(V,D_{n},M_{n},t_{n})$, if and only if there exists a matching
function $\gamma:M_{n}\to[1,\ldots,n]$ such that, for every atom of the form
$T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$ in $\mathsf{C}$:

  1. (I)

if $T^{\prime}\in M_{n}$, then also $T\in M_{n}$,
$\gamma(T)\leq\gamma(T^{\prime})$, and
$l\leq\delta({\overline{\mu}}_{[\gamma(T)\ldots\gamma(T^{\prime})]})\leq u$;

  2. (II)

if $T^{\prime}\not\in M_{n}$, but $T\in M_{n}$, then
$\delta({\overline{\mu}}_{[\gamma(T)\ldots n]})\leq u$.

Furthermore, $\gamma$ and ${\overline{}{I}}$ are such that for every $T\in
M_{n}$, $T\in I_{\gamma(T)}$, , they agree on the matching of the terms of
$\mathsf{M}_{n}$. We write
$M_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma}M_{n}$, if $\gamma$
corresponds to a run of $\mathsf{M}_{\mathsf{E}}$, or
${\overline{\mu}},\gamma\models\mathsf{M}_{n}$, if $\mathsf{M}_{\mathsf{E}}$
is clear from the context.

######  Observation 1.

Note that the existence of the matching function $\gamma$ stated by Lemma 2,
if the corresponding matching structure is closed, implies the satisfaction of
the given existential statement, and .

We now state the core technical result of the completeness proof, which
ensures no important details are lost when matching structures are discarded.

######  Lemma 3.

Let ${\overline{\mu}}=\langle{\mu}_{1},\dots,{\mu}_{n}\rangle$ be an event
sequence , let $\mathsf{M}_{\mathsf{E}}$ be the initial matching structure of
some existential statement $\mathsf{E}$ of a rule $\mathsf{R}$, and let
$\mathsf{M}_{r}$ be an active matching structure resulting from a run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma_{r}}\mathsf{M}_{r}$,
such that $\gamma_{r}(\operatorname{start}(a_{0}))=r$. If there exists a run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma_{s}}\mathsf{M}_{s}$,
such that $\gamma_{s}(\operatorname{start}(a_{0}))<r$, then there exists a run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma}\mathsf{M}$,
such that
$\gamma(\operatorname{start}(a_{0}))=\gamma_{s}(\operatorname{start}(a_{0}))$
and $\mathsf{M}$ matches at least as many tokens as $\mathsf{M}_{r}$.

The last needed notion is that of _residual_ matching structure, which is an
active matching structure with only infinite bounds.

[Residual matching structure] A matching structure $\mathsf{M}=(V,D,M,t)$ is
_residual_ if it is _active_ and for every $T\in M$ and
$T^{\prime}\in\overline{M}$, $D[T^{\prime},T]=+\infty$.

In other words, $\mathsf{M}$ does not impose any finite upper bound on the
distance at which terms yet to be matched may appear relative to those already
matched. The definition implies that for any residual matching structure,
denoted as $\hat{}\mathsf{M}=(V,D,M,t)$, every event ${\mu}=(A,\delta)$ is
admissible. Additionally, it is never the case that
$\operatorname{start}(a)\in M$ and $\operatorname{end}(a)\in\overline{M}$ for
any quantified token $a[x=v]$ of $\mathsf{E}$, given that such terms always
have a finite upper bound in $D$ that is at least as strict as the value
$d^{x=v}_{max\vphantom{i}}$. As a result, the “if” direction of Item 1b in the
Figure 2 of $I$-match never applies to $\hat{}\mathsf{M}$ for any event
${\mu}$. Therefore, every event is a valid $\varnothing$-match event for
$\hat{}\mathsf{M}$.

######  Observation 2.

Let
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}}_{1},{\overline{}{I}}_{1}}\hat{}\mathsf{M}$
be a run of the _initial_ matching structure $\mathsf{M}_{\mathsf{E}}$, on an
event sequence ${\overline{\mu}}_{1}$, yielding a _residual_ matching
structure $\hat{}\mathsf{M}$. Then, for any event sequence
${\overline{\mu}}_{2}$, there exists a run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}}_{1}{\overline{\mu}}_{2},{\overline{}{I}}_{1}{\overline{}{I}}_{2}}\hat{}\mathsf{M}^{\prime}$
such that every $I$-match event in ${\overline{}{I}}_{2}$ is an
$\varnothing$-match event and $\hat{}\mathsf{M}^{\prime}$ differs from
$\hat{}\mathsf{M}$ by at most the value of the component $t$.

Consequently, whenever a residual matching structure appears in a run, it has
the potential to remain there indefinitely, which is why it is called
_residual_.

######  Lemma 4 (Existence of residual matching structure).

Let ${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ be an event
sequence, and let $\mathsf{M}_{n}$ be an _active_ matching structure such that
${\overline{\mu}},\gamma\models\mathsf{M}_{n}$ and
$\delta({\overline{\mu}}_{[\gamma(\operatorname{start}(a_{0}))\ldots
n]})>\operatorname{window}(P)$. If we consider the intermediate matching
structures $\langle\mathsf{M}_{1},\ldots,\mathsf{M}_{n-1}\rangle$ of the run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma}\mathsf{M}_{n}$,
then there exists a position $\gamma(\operatorname{start}(a_{0}))\leq k<n$
such that $\mathsf{M}_{k}$ is a _residual_ matching structure.

We are now ready to prove the final result.

######  Theorem 5 (Soundness and completeness).

Let $P=(\mathsf{SV},S)$ be a timeline-based planning problem and let
$\mathsf{A}_{P}$ be the associated automaton. Then, any event sequence
${\overline{\mu}}$ is a solution plan for $P$ if and only if
${\overline{\mu}}$ is accepted by $\mathsf{A}_{P}$.

##  5\. Controller synthesis

We leverage the deterministic automaton constructed in the previous section to
establish a deterministic arena that enables us to solve a reachability game
and determine whether a controller exists. If a controller exists, our
procedure allows its synthesis.

###  5.1. From the automaton to the arena

Let $G=(\mathsf{SV}_{C},\mathsf{SV}_{E},\mathsf{S},\mathsf{D})$ be a timeline-
based game. The automaton construction we used considered a planning problem
with a single set of synchronization rules, while in $G$, we have to account
for the roles of both $\mathsf{S}$ and $\mathsf{D}$.

To address this, we define $A_{\mathsf{S}}$ and $A_{\mathsf{D}}$ as the
deterministic automata constructed over the timeline-based planning problems
$P_{\mathsf{S}}=(\mathsf{SV}_{C}\cup\mathsf{SV}_{E},\mathsf{S})$ and
$P_{\mathsf{D}}=(\mathsf{SV}_{C}\cup\mathsf{SV}_{E},\mathsf{D})$,
respectively. We then construct the automaton $A_{G}$ by taking the union of
$A_{\mathsf{S}}$ with the complement of $A_{\mathsf{D}}$
($\overline{A_{\mathsf{D}}}$). Note that these are standard automata-theoretic
operations over DFAs. An accepting run of $A_{G}$ represents either a plan
that violates the domain rules or a plan that adheres to domain and system
rules, according to the definition of winning strategy in Section 3.2.
Furthermore, $A_{G}$ is deterministic, and its size only polynomially
increases when built from $A_{\mathsf{D}}$ and $A_{\mathsf{S}}$.

The $A_{G}$ automaton is not immediately applicable as a game arena since its
transitions’ labels only reflect events, not game moves. In $A_{G}$, a single
transition can correspond to various combinations of rounds due to the absence
of $\operatorname{wait}(\delta)$ moves in the transition’s label. For example,
an event ${\mu}=(A,5)$ can arise from either a $\operatorname{wait}(5)$ move
by _Charlie_ , followed by a $\operatorname{play}(5,A)$ move by Eve, or any
$\operatorname{wait}(\delta)$ move with $\delta>5$ followed by a
$\operatorname{play}(5,A)$ move. To obtain a suitable game arena, we need to
modify $A_{G}$ further.

Let $A_{G}=(Q,\Sigma,q_{0},F,\tau)$ be the automaton constructed as described
above. Formally, we define a new automaton
$A_{G}^{\prime}=(Q,\Sigma,q_{0},F,\tau^{\prime})$ where $\tau^{\prime}$ is a
partial transition function, meaning that the automaton is now incomplete. The
function $\tau^{\prime}$ agrees with $\tau$ on all transitions except those of
the form $\tau(q,(\mathsf{A},\delta))$, where $\delta>1$ and $\mathsf{A}$
contains a $\operatorname{end}(x,v)$ action with $x\in\mathsf{SV}_{C}$. In
such cases, the transition is undefined in $A_{G}^{\prime}$. An example is
shown in Figure 4 (left). Note that this removal does not alter the set of
plans accepted by the automaton since for each transition
$\tau(q,(\mathsf{A},\delta))=q^{\prime}$ with $\delta>1$, there exist two
transitions $\tau(q,(\varnothing,\delta-1))=q^{\prime\prime}$ and
$\tau(q^{\prime\prime},(\mathsf{A},1))=q^{\prime}$ in $A_{G}^{\prime}$.

${\mu}=(\\{\operatorname{end}(x,v)\\},5)$ ${\mu}^{\prime}=(\varnothing,4)$
${\mu}^{\prime\prime}=(\\{\operatorname{end}(x,v)\\},1)$
$q$$w$${\mu}=(\\{\operatorname{end}(x,v_{1}),\operatorname{end}(y,w_{1}),\operatorname{start}(x,v_{2}),\operatorname{start}(y,w_{2})\\},5)$
$\operatorname{wait}(5)$ $\operatorname{wait}(6)$ $\operatorname{wait}(7)$
$\operatorname{wait}(10)$
$\operatorname{play}\left(5,\left\\{\begin{array}[]{@{}c@{}}\operatorname{end}(x,v_{1})\\\
\operatorname{end}(y,w_{1})\end{array}\right\\}\right)$
$\operatorname{play}\left(5,\left\\{\begin{array}[]{@{}c@{}}\operatorname{end}(x,v_{1})\\\
\operatorname{end}(y,w_{1})\end{array}\right\\}\right)$
$\operatorname{play}(\\{\operatorname{start}(x,v_{2})\\})$
$\operatorname{play}(\\{\operatorname{start}(y,w_{2})\\})$ Figure 4. On the
left, the removal of transitions ${\mu}=(A,\delta)$ with $\delta>1$ and ending
actions of controllable tokens in $A$. On the right, the transformation of a
transition of $A_{G}$ into a sequence of transitions in $A^{a}_{G}$, with
$x\in\mathsf{SV}_{C}$, $y\in\mathsf{SV}_{E}$, and
$\gamma_{x}(v_{1})=\gamma_{y}(w_{1})=\mathsf{u}$.

To make the game rounds and moves explicit, we can transform the automaton by
splitting each transition into four transitions representing the four moves of
the two rounds. Starting from the incomplete automaton
$A_{G}^{\prime}=(Q,\Sigma,q_{0},F,\tau^{\prime})$, we define a new automaton
$A_{G}^{a}=(Q^{a},\Sigma^{a},q_{0}^{a},F^{a},\tau^{a})$ as the game arena.

  1. (1)

The set of states $Q^{a}$ is given by $Q^{a}=Q\cup\\{q_{\delta}\mid
1\leq\delta\leq d\\}\cup\\{q_{\delta,A}\mid 1\leq\delta\leq
d,A\subseteq\mathsf{A}\\}$.

  2. (2)

The alphabet $\Sigma^{a}$ is defined as
$\Sigma^{a}=\mathcal{M}_{C}\cup\mathcal{M}_{E}$, which corresponds to the set
of moves of the two players.

  3. (3)

The initial and final states of $A_{G}^{a}$ are $q_{0}^{a}=q_{0}$ and
$F^{a}=F$, respectively.

  4. (4)

The partial transition function $\tau^{a}$ is defined as follows. Let
$w=\tau(q,{\mu})$ with ${\mu}=(\mathsf{A},\delta)$. We distinguish the cases
where $\delta=1$ or $\delta>1$.

    1. (a)

if $\delta=1$, let $\mathsf{A}_{C}\subseteq\mathsf{A}$ and
$\mathsf{A}_{E}\subseteq\mathsf{A}$ be the set of actions in $\mathsf{A}$
playable by _Charlie_ and by _Eve_ , respectively. Then:

      1. (i)

$\tau(q,\operatorname{play}(\mathsf{A}_{C}^{e}))=q_{1,\mathsf{A}_{C}^{e}}$,
where $\mathsf{A}_{C}^{e}$ is the set of _ending_ actions in $\mathsf{A}_{C}$;

      2. (ii)

$\tau(q_{1,\mathsf{A}_{C}^{e}},\operatorname{play}(\mathsf{A}_{E}^{e}))=q_{1,\mathsf{A}_{C}^{e}\cup\mathsf{A}_{E}^{e}}$,
where $\mathsf{A}_{E}^{e}$ is the set of _ending_ actions in $\mathsf{A}_{E}$;

      3. (iii)

$\tau(q_{1,\mathsf{A}_{C}^{e}\cup\mathsf{A}_{E}^{e}},\operatorname{play}(\mathsf{A}_{C}^{s}))=q_{1,\mathsf{A}_{C}^{e}\cup\mathsf{A}_{E}^{e}\cup\mathsf{A}_{C}^{s}}$,
where $\mathsf{A}_{C}^{s}$ is the set of _starting_ actions in
$\mathsf{A}_{C}$;

      4. (iv)

$\tau(q_{1,\mathsf{A}_{C}^{e}\cup\mathsf{A}_{E}^{e}\cup\mathsf{A}_{C}^{s}},\operatorname{play}(\mathsf{A}_{E}^{s}))=w$,
where $\mathsf{A}_{E}^{s}$ is the set of _starting_ actions in
$\mathsf{A}_{E}$;

Here, the states mentioned are added to $Q^{a}$ as needed.

    2. (b)

if $\delta>1$, let $\mathsf{A}_{C}\subseteq\mathsf{A}$ and
$\mathsf{A}_{E}\subseteq\mathsf{A}$ be the set of actions in $\mathsf{A}$
playable by _Charlie_ and by _Eve_ , respectively. Note that by construction,
$\mathsf{A}_{C}$ only contains _starting_ actions. Then:

      1. (i)

$\tau(q,\operatorname{wait}(\delta_{C}))=q_{\delta_{C}}$ for all
$\delta\leq\delta_{C}\leq d$;

      2. (ii)

$\tau(q_{\delta_{C}},\operatorname{play}(\delta,\mathsf{A}_{E}^{e}))=q_{\delta,\mathsf{A}_{E}^{e}}$
where $\mathsf{A}_{E}^{e}$ is the set of _ending_ actions in $\mathsf{A}_{E}$;

      3. (iii)

$\tau(q_{\delta,\mathsf{A}_{E}^{e}},\operatorname{play}(\mathsf{A}_{C}))=q_{\delta,\mathsf{A}_{E}^{e}\cup\mathsf{A}_{C}}$;

      4. (iv)

$\tau(q_{\delta,\mathsf{A}_{E}^{e}\cup\mathsf{A}_{C}},\operatorname{play}(\mathsf{A}_{E}^{s}))=w$
where $\mathsf{A}_{E}^{s}$ is the set of _starting_ actions in
$\mathsf{A}_{E}$;

where the mentioned states are added to $Q^{a}$ as needed.

All the transitions not explicitly defined above are undefined.

We present a graphical illustration of the above construction in Fig. 4. It is
worth noting that the automaton preserves the structure of the original
automaton $A_{G}$. For any state, $q\in Q$ and event ${\mu}=(A,\delta)$, any
sequence of moves that would result in appending ${\mu}$ to the partial plan
(see Section 3.2) reaches the same state $w$ in $A^{a}_{G}$ as it does in
$A_{G}$ by reading ${\mu}$. Therefore, we can consider $A^{a}_{G}$ as being
able to read event sequences, even though its alphabet is different. We use
the notation $[{\overline{\mu}}]$ to represent the state $q\in Q^{a}$ reached
by reading ${\overline{\mu}}$ in $A^{a}_{G}$. Furthermore, note that, with a
slight abuse of notation, any play $\overline{\rho}$ in the game $G$ is a
readable word by the automaton $A_{G}^{a}$. Thus, we can establish the
following result.

######  Theorem 6.

If $G$ is a timeline-based game, for any play $\overline{\rho}$ for $G$,
$\overline{\rho}$ is successful if and only if it is accepted by $A_{G}^{a}$.

###  5.2. Computing the Winning Strategy and Building the Controller

Let us define $Q^{a}_{C}\subset Q^{a}$ as the set of states in which _Charlie_
can make a move, and $Q^{a}_{E}=Q^{a}\setminus Q^{a}_{C}$ as the set of states
where _Eve_ can make a move. Additionally, we define $E=\\{(q,q^{\prime})\in
Q^{a}\times Q^{a}\mid\exists{\mu}\mathrel{.}\tau^{a}(q,{\mu})=q^{\prime}\\}$
as the set of edges in $A^{a}_{G}$. By solving the reachability game
$(G_{R},\mathcal{W})$, where $G_{R}=(Q^{a},Q^{a}_{C},E^{a})$ and
$\mathcal{W}=\\{R\subseteq Q^{a}\mid R\cap F^{a}\neq\varnothing\\}$, we aim to
determine the winning region $W_{C}$ and the winning strategy $s_{C}$ for
_Charlie_ , provided they exist. In the following discussion, we will show
that the winning strategy $\sigma_{C}$ for the timeline-based game $G$ is
derivable from strategy $s_{C}$ when $q^{a}_{0}\in W_{C}$.

To determine the winning region $W_{C}$, we use the well-known _attractor_
construction. We are interested to the attractor set of $F^{a}$ for _Charlie_
, written $Attr_{C}(F^{a})$, thus given $i\geq 0$ we compute the set of states
from which _Charlie_ can reach a state $q\in F^{a}$ within $i$ moves, defined
as $Attr_{C}^{i}(F^{a})$:

$\displaystyle Attr^{0}_{C}(F^{a})$ $\displaystyle=F^{a}$ $\displaystyle
Attr^{i+1}_{C}(F^{a})$ $\displaystyle=Attr^{i}_{C}(F^{a})$
$\displaystyle\cup\\{q^{a}\in Q^{a}_{C}\,|\,\exists r\big{(}(q^{a},r)\in
E\land r\in Attr^{i}_{C}(F^{a})\big{)}\\}$ $\displaystyle\cup\\{q^{a}\in
Q^{a}_{E}\,|\,\forall r\big{(}(q^{a},r)\in E\rightarrow r\in
Attr^{i}_{C}(F^{a})\big{)}\\}.$

The sequence $Attr^{0}_{C}(F^{a})\subseteq Attr^{1}_{C}(F^{a})\subseteq
Attr^{2}_{C}(F^{a})\subseteq\ldots$ eventually becomes stationary for some
index $k\leq\lvert Q^{a}\rvert$, hence we can define
$Attr_{C}(F^{a})=\bigcup^{\lvert Q^{a}\rvert}_{i=0}Attr^{i}_{C}(F^{a})$ as the
attractor set. Note that $W_{C}=Attr_{C}(F^{a})$ is a known fact for which
proof is available in [Tho08]. Next, we want that $q_{0}^{a}\in W_{C}$ since
we are interested in a winning strategy $\sigma_{C}$ for the timeline-based
game $G$. If it is the case, by defining $s_{C}(q)=\mu$ for any $\mu$ such
that $\tau^{a}(q,\mu)=q^{\prime}$ with $q,q^{\prime}\in W_{C}$, which is
guaranteed to exist by the attractor construction, we can define $\sigma_{C}$
for _Charlie_ in $G$ as
$\sigma_{C}({\overline{\mu}})=s_{C}([{\overline{\mu}}])$ for any event
sequence ${\overline{\mu}}$. We prove this claim in the following:

######  Theorem 7.

Given $A_{G}^{a}=(Q^{a},\Sigma^{a},q_{0}^{a},F^{a},\tau^{a})$, $q_{0}^{a}\in
W_{C}$ if and only if $\sigma_{C}$ is a winning strategy for _Charlie_ for
$G$.

######  Proof 5.1.

$(\longleftarrow)$. From the definition of a winning strategy for _Charlie_ in
$G$ (Section 3.2), we know that for every admissible strategy $\sigma_{E}$ for
_Eve_ , there exists $n\geq 0$ such that the play
${\overline{\rho}}_{n}({\sigma}_{C},{\sigma}_{E})$ is successful. By the
soundness of the arena construction (Theorem 6), we know that the event
sequence ${\overline{\mu}}_{n}$ representing
${\overline{\rho}}_{n}({\sigma}_{C},{\sigma}_{E})$, when seen as a word over
$\Sigma^{a}$, is accepted by $A_{G}^{a}$. Therefore, ${\overline{\mu}}_{n}$
reaches a state in the set $F^{a}$ starting from $q_{0}^{a}$. By the
definition of the reachability game, this means that $q_{0}^{a}\in W_{C}$.
Thus, we have proved that if $\sigma_{C}$ is a winning strategy _Charlie_ in
$G$, then $q_{0}^{a}\in W_{C}$.

$(\longrightarrow)$. If $q_{0}^{a}\in W_{C}$, then by definition, $s_{C}$ is a
winning strategy for _Charlie_ in the reachability game over the arena
$A_{G}^{a}$. Hence, any word over $\Sigma^{a}$ obtained by playing with
$s_{C}$ is accepted by $A_{G}^{a}$, and therefore, by the soundness of the
arena construction (Theorem 6), any corresponding play ${\overline{\rho}}$ is
successful in $G$. Now, recall that
$\sigma_{C}({\overline{\mu}})=s_{C}([{\overline{\mu}}])$ for any event
sequence ${\overline{\mu}}$. Hence,
${\overline{\rho}}={\overline{\rho}}(\sigma_{C},\sigma_{E})$ for some strategy
$\sigma_{E}$ of _Eve_. As a result, we can conclude that $\sigma_{C}$ is a
winning strategy for _Charlie_ in $G$.

Finally, we build a Controller that implements the winning strategy
$\sigma_{C}$, provided it exists. First, by Theorem 7, the existence of
$\sigma_{C}$ implies that $q^{a}_{0}\in W_{C}$. Next, we define the following
Moore machine (Section 3.3) based on $s_{C}$:

[Controller] Given $A_{G}^{a}=(Q^{a},\Sigma^{a},q_{0}^{a},F^{a},\tau^{a})$, we
define a Controller as $\mathcal{M}=(Q,\Sigma,\Gamma,q_{0},\delta,\tau)$,
where $Q=Q^{a}_{C}\cap W_{C}$ represents the set of states, $q_{0}=q_{0}^{a}$
is the initial state, $\Sigma=\mathcal{M}_{E}$ is the input alphabet,
$\Gamma=\mathcal{M}_{C}$ is the output alphabet,
$\delta:Q\times\Sigma\rightarrow Q$ is the transition function, and
$\tau:Q\rightarrow\Gamma$ is the output function. The transition function
$\delta$ and the output function $\tau$ are defined as follows:

$\displaystyle\delta(q_{C},{\mu}_{E})$
$\displaystyle=\tau^{a}(s_{C}(q_{C}),{\mu}_{E})$ $\displaystyle\tau(q_{C})$
$\displaystyle=s_{C}(q_{C}).$

Note that by construction the states of $\mathcal{M}$ belong to the winning
region $W_{C}$ of $A_{G}^{a}$, and $\delta$ follows the transition function
$\tau^{a}$ of $A^{a}_{G}$. Hence, the output of $\mathcal{M}$ after reading a
word ${\overline{\mu}}$ is exactly
$\sigma_{C}({\overline{\mu}})=s_{C}([{\overline{\mu}}])$ and $\mathcal{M}$
implements $\sigma_{C}$, which is a winning strategy by Theorem 7.

##  6\. Conclusions and Future Work

Our article presents an effective procedure for synthesizing controllers for
timeline-based games, whereas previously, only a proof of the
$\mathsf{2EXPTIME}$-completeness of the problem of determining the existence
of a strategy was available in the literature. We use a novel construction of
a _deterministic_ automaton of doubly-exponential (thus optimal) size, which
is then adapted to serve as the arena for the game. Then, with standard
methods, we solve a reachability game on the arena to effectively compute the
winning strategy for the game, if it exists.

This work paves the way for future developments. First, the procedure provided
in this article can be realistically implemented and tested. It is
conceivable, though, that to avoid the state explosion problem due to the
doubly-exponential size of the automaton, it will be necessary to apply
_symbolic techniques_. Moreover, an implementation would also need a concrete
syntax to specify timeline-based games. Existing languages supported by
timeline-based systems (NDDL [CO96] or ANML [SFC08]) might be inadequate for
this purpose. Next, as in the case of $\mathsf{LTL}$, the high complexity
makes one wonder whether simpler but still expressive fragments can be found.
One possibility might be restricting the synchronization rules to only talk
about the _past_ concerning the rule’s trigger. For co-safety properties
(properties expressing the fact that something good will eventually happen)
expressed in pure-past $\mathsf{LTL}$, the realizability problem goes down to
being $\mathsf{EXPTIME}$-complete, and by analogy, this might happen to pure-
past timeline-based games as well.

## Acknowledgements

Luca Geatti, Nicola Gigante, and Angelo Montanari acknowledge the support from
the GNCS project: “Strategic reasoning and automatic synthesis of multi-agent
systems”. Nicola Gigante and Luca Geatti also acknowledge the support of the
Free University of Bozen-Bolzano, Faculty of Computer Science, by means of the
projects TOTA (_Temporal Ontologies and Tableaux Algorithms_) and STAGE
(_Synthesis of Timeline-based Planning Games_). Nicola Gigante acknowledges
the support of the PURPLE project, 1st Open Call for Innovators of the
AIPlan4EU H2020 project, a project funded by EU Horizon 2020 research and
innovation programme under GA n. 101016442.

## References

  * [AGG+22] Renato Acampora, Luca Geatti, Nicola Gigante, Angelo Montanari, and Valentino Picotti.  Controller synthesis for timeline-based games.  Electronic Proceedings in Theoretical Computer Science, 370:131–146, sep 2022.  URL: https://doi.org/10.42042Feptcs.370.9, ${\overline{T}}$doi:10.4204/eptcs.370.9.
  * [AHK02] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman.  Alternating-time temporal logic.  J. ACM, 49(5):672–713, 2002.  ${\overline{T}}$doi:10.1145/585265.585270.
  * [BL90] J Richard Buchi and Lawrence H Landweber.  Solving sequential conditions by finite-state strategies.  In The Collected Works of J. Richard Büchi, pages 525–541. Springer, 1990.
  * [BMM+20] Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Gerhard J. Woeginger.  Timeline-based planning over dense temporal domains.  Theor. Comput. Sci., 813:305–326, 2020.  ${\overline{T}}$doi:10.1016/j.tcs.2019.12.030.
  * [BS07] Sara Bernardini and David E. Smith.  Developing domain-independent search control for Europa2.  In Proceedings of the ICAPS 2007 Workshop on Heuristics for Domain-Independent Planning, 2007.
  * [BWMB+05] Tania Bedrax-Weiss, Conor McGann, Andrew Bachmann, Will Edgington, and Michael Iatauro.  Europa2: User and contributor guide.  Technical report, NASA Ames Research Center, 2005.
  * [Byl94] Tom Bylander.  The computational complexity of propositional STRIPS planning.  Artificial Intelligence, 69(1-2):165–204, 1994.  ${\overline{T}}$doi:10.1016/0004-3702(94)90081-7.
  * [CCD+07] Amedeo Cesta, Gabriella Cortellessa, Michel Denis, Alessandro Donati, Simone Fratini, Angelo Oddi, Nicola Policella, Erhard Rabenau, and Jonathan Schulster.  MEXAR2: AI solves mission planner problems.  IEEE Intelligent Systems, 22(4):12–19, 2007.  ${\overline{T}}$doi:10.1109/MIS.2007.75.
  * [CCF+06] Amedeo Cesta, Gabriella Cortellessa, Simone Fratini, Angelo Oddi, and Nicola Policella.  Software companion: The MEXAR2 support to space mission planners.  In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors, Proceedings of the 17th European Conference on Artificial Intelligence, volume 141 of Frontiers in Artificial Intelligence and Applications, pages 622–626. IOS Press, 2006.
  * [Chu62] Alonzo Church.  Logic, arithmetic, and automata.  In Proceedings of the international congress of mathematicians, volume 1962, pages 23–35, 1962.
  * [CO96] Amedeo Cesta and Angelo Oddi.  Ddl.1: A formal description of a constraint representation language for physical domains.  In Malik Ghallab and Alfredo Milani, editors, New directions in AI planning. IOS Press, 1996.
  * [COU16] Marta Cialdea Mayer, Andrea Orlandini, and Alessandro Umbrico.  Planning and execution with flexible timelines: a formal account.  Acta Informatica, 53(6-8):649–680, 2016.  ${\overline{T}}$doi:10.1007/s00236-015-0252-z.
  * [CRK+00] S. Chien, G. Rabideau, R. Knight, R. Sherwood, B. Engelhardt, D. Mutz, T. Estlin, B. Smith, F. Fisher, T. Barrett, G. Stebbins, and D. Tran.  Aspen - automating space mission operations using automated planning and scheduling.  In Proceedings of the International Conference on Space Operations, 2000.
  * [CRT+15] Steve A. Chien, Gregg Rabideau, Daniel Tran, Martina Troesch, Joshua Doubleday, Federico Nespoli, Miguel Perez Ayucar, Marc Costa Sitja, Claire Vallat, Bernhard Geiger, Nico Altobelli, Manuel Fernandez, Fran Vallejo, Rafael Andres, and Michael Kueppers.  Activity-based scheduling of science campaigns for the rosetta orbiter.  In Qiang Yang and Michael Wooldridge, editors, Proceedings of the 24th International Joint Conference on Artificial Intelligence, pages 4416–4422. AAAI Press, 2015.  URL: http://ijcai.org/Abstract/15/655.
  * [DGM+17] Dario Della Monica, Nicola Gigante, Angelo Montanari, Pietro Sala, and Guido Sciavicco.  Bounded timed propositional temporal logic with past captures timeline-based planning with bounded constraints.  In Carles Sierra, editor, Proceedings of the 26th International Joint Conference on Artificial Intelligence, pages 1008–1014, 2017.  ${\overline{T}}$doi:10.24963/ijcai.2017/140.
  * [DGMS18] Dario Della Monica, Nicola Gigante, Angelo Montanari, and Pietro Sala.  A novel automata-theoretic approach to timeline-based planning.  In Michael Thielscher, Francesca Toni, and Frank Wolter, editors, Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning, pages 541–550. AAAI Press, 2018.  URL: https://aaai.org/ocs/index.php/KR/KR18/paper/view/18024.
  * [DGTM20] Dario Della Monica, Nicola Gigante, Salvatore La Torre, and Angelo Montanari.  Complexity of qualitative timeline-based planning.  In Proceedings of the 27th International Symposium on Temporal Representation and Reasoning, volume 178 of LIPIcs, pages 16:1–16:13, 2020\.  ${\overline{T}}$doi:10.4230/LIPIcs.TIME.2020.16.
  * [Dil89] David L. Dill.  Timing assumptions and verification of finite-state concurrent systems.  In Joseph Sifakis, editor, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197–212. Springer, 1989\.  ${\overline{T}}$doi:10.1007/3-540-52148-8_17.
  * [DPC+08] Alessandro Donati, Nicola Policella, Amedeo Cesta, Simone Fratini, Angelo Oddi, Gabriella Cortellessa, Federico Pecora, Jonathan Schulster, Erhard Rabenau, Marc Niezette, and Robin Steel.  Science operations pre-planning & optimization using ai constraint-resolution - the apsi case study 1.  In Proceedings of the 8th International Conference on Space Operations, 2008.  ${\overline{T}}$doi:10.2514/6.2008-3268.
  * [FCO+11] Simone Fratini, Amedeo Cesta, Andrea Orlandini, Riccardo Rasconi, and Riccardo De Benedictis.  Apsi-based deliberation in goal oriented autonomous controllers.  In ASTRA 2011, volume 11. ESA, 2011.
  * [FJ03] Jeremy Frank and Ari K. Jónsson.  Constraint-based attribute and interval planning.  Constraints, 8(4):339–364, 2003.  ${\overline{T}}$doi:10.1023/A:1025842019552.
  * [FL03] Maria Fox and Derek Long.  PDDL2.1: An extension to PDDL for expressing temporal planning domains.  Journal of Artificial Intelligence Research, 20:61–124, 2003\.
  * [FN71] Richard Fikes and Nils J. Nilsson.  STRIPS: A new approach to the application of theorem proving to problem solving.  Artificial Intelligence, 2(3/4):189–208, 1971.  ${\overline{T}}$doi:10.1016/0004-3702(71)90010-5.
  * [Gig19] Nicola Gigante.  Timeline-based Planning: Expressiveness and Complexity.  PhD thesis, University of Udine, Italy, 2019.  Available on _arXiv_ at: https://arxiv.org/abs/1902.06123.
  * [GMCO16] Nicola Gigante, Angelo Montanari, Marta Cialdea Mayer, and Andrea Orlandini.  Timelines are expressive enough to capture action-based temporal planning.  In Curtis E. Dyreson, Michael R. Hansen, and Luke Hunsberger, editors, Proceedings of the 23rd International Symposium on Temporal Representation and Reasoning, pages 100–109. IEEE Computer Society, 2016.  ${\overline{T}}$doi:10.1109/TIME.2016.18.
  * [GMCO17] Nicola Gigante, Angelo Montanari, Marta Cialdea Mayer, and Andrea Orlandini.  Complexity of timeline-based planning.  In Laura Barbulescu, Jeremy Frank, Mausam, and Stephen F. Smith, editors, Proceedings of the 27th International Conference on Automated Planning and Scheduling, pages 116–124. AAAI Press, 2017.  URL: https://aaai.org/ocs/index.php/ICAPS/ICAPS17/paper/view/15758.
  * [GMO+20] Nicola Gigante, Angelo Montanari, Andrea Orlandini, Marta Cialdea Mayer, and Mark Reynolds.  On timeline-based games and their complexity.  Theor. Comput. Sci., 815:247–269, 2020.  ${\overline{T}}$doi:10.1016/j.tcs.2020.02.011.
  * [MH69] John McCarthy and Patrick J. Hayes.  Some philosophical problems from the standpoint of artificial intelligence.  In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 463–502. Edinburgh University Press, 1969.
  * [Mus94] Nicola Muscettola.  HSTS: Integrating Planning and Scheduling.  In Monte Zweben and Mark S. Fox, editors, Intelligent Scheduling, chapter 6, pages 169–212. Morgan Kaufmann, 1994.
  * [OFCF11] Andrea Orlandini, Alberto Finzi, Amedeo Cesta, and Simone Fratini.  Tga-based controllers for flexible plan execution.  In Joscha Bach and Stefan Edelkamp, editors, Proceedings of the 34th Annual German Conference on Artificial Intelligence, volume 7006 of Lecture Notes in Computer Science, pages 233–245. Springer, 2011.  ${\overline{T}}$doi:10.1007/978-3-642-24455-1_22.
  * [PH07] Mathias Péron and Nicolas Halbwachs.  An abstract domain extending difference-bound matrices with disequality constraints.  In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 268–282. Springer, 2007.  ${\overline{T}}$doi:10.1007/978-3-540-69738-1_20.
  * [PR89a] A. Pnueli and R. Rosner.  On the synthesis of a reactive module.  In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’89, page 179–190, New York, NY, USA, 1989. Association for Computing Machinery.  ${\overline{T}}$doi:10.1145/75277.75293.
  * [PR89b] Amir Pnueli and Roni Rosner.  On the synthesis of an asynchronous reactive module.  In International Colloquium on Automata, Languages, and Programming, pages 652–671. Springer, 1989.
  * [Ros92] Roni Rosner.  Modular synthesis of reactive systems.  PhD thesis, Weizmann Institute of Science, 1992.
  * [SFC08] David E. Smith, Jeremy Frank, and William Cushing.  The ANML language.  In Proceedinsgs of the ICAPS 2008 Workshop on Knowledge Engineering for Planning and Scheduling, 2008.
  * [Tho08] Wolfgang Thomas.  Solution of Church’s problem: A tutorial.  New Perspectives on Games and Interaction. Texts on Logic and Games, 5, 2008.

##  7\. Appendix

See 2

######  Proof 7.1.

$(\longleftarrow)$. We proceed by induction on the length of the event
sequence ${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$.

Base case:

If $n=0$, the only well defined function on an empty codomain is the function
$\gamma_{0}:\varnothing\to\varnothing$ with an empty domain, which vacuously
satisfies the definition of matching function and Items (I) and (II). Then,
the only run of $\mathsf{M}_{\mathsf{E}}=(V,D,\varnothing,0)$ on an empty
event sequence ${\overline{\mu}}$ is the empty run ${\overline{}{I}}$ yielding
$\mathsf{M}_{\mathsf{E}}$ itself, which vacuously satisfies the definition of
run.

Inductive step:

Let $\gamma:M_{n}\to[1,\ldots,n]$ be a matching function satisfying Items (I)
and (II), and let $\gamma|^{<n}:M_{n-1}\to[1,\ldots,n-1]$ be the restriction
of $\gamma$ on the domain $M_{n-1}$ defined as the inverse image of
$[1,\ldots,n-1]$ under $\gamma$, , $M_{n-1}=\gamma^{-1}([1,\ldots,n-1])$.
$\gamma|^{<n}$ is a matching function for the event sequence
${\overline{\mu}}_{[1\ldots n-1]}$ and satisfies Items (I) and (II). By the
inductive hypothesis, there exists a run $\langle I_{1},\ldots,I_{n-1}\rangle$
of $\mathsf{M}_{\mathsf{E}}$ on ${\overline{\mu}}_{[1\ldots n-1]}$, yielding a
matching structure $\mathsf{M}_{n-1}=(V,D_{n-1},M_{n-1},t_{n-1})$. Let
$I_{n}=\gamma^{-1}(n)$, and note that $I_{n}\subseteq\overline{M_{n-1}}$. We
show that ${\mu}_{n}=(A_{n},\delta_{n})$ is an _$I_{n}$ -match_ event for
$\mathsf{M}_{n-1}$ by breaking the proof in steps.

(Step: ${\mu}_{n}$ is an _admissible_ event for $\mathsf{M}_{n-1}$). Let $T\in
M_{n-1}$ and $T^{\prime}\not\in M_{n-1}$. If $D_{n-1}[T^{\prime},T]=+\infty$,
$\delta_{n}\leq D_{n-1}[T^{\prime},T]$ trivially holds. Otherwise, there
exists an atom $T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$ in $\mathsf{C}$
and $D_{n-1}[T^{\prime},T]=u-\delta({\overline{\mu}}_{[\gamma|^{<n}(T)\ldots
n-1]})$. We consider two cases based on whether $T^{\prime}$ belongs to the
domain of $\gamma$, or not. In the first case, $\gamma(T^{\prime})=n$ and
$\delta({\overline{\mu}}_{[\gamma(T)\ldots
n-1]})+\delta_{n}=\delta({\overline{\mu}}_{[\gamma(T)\ldots\gamma(T^{\prime})]})\leq
u$, by Item (I). In the second case,
$\delta({\overline{\mu}}_{[\gamma(T)\ldots
n-1]})+\delta_{n}=\delta({\overline{\mu}}_{[\gamma(T)\ldots n]})\leq u$, by
Item (II). In either case, $\delta_{n}\leq
u-\delta({\overline{\mu}}_{[\gamma(T)\ldots n-1]})=D_{n-1}[T^{\prime},T]$.

(Step: Item 1a of Figure 2). Let $a[x=v]$ be a quantified token of
$\mathsf{E}$. If $\operatorname{start}(a)\in I_{n}$, then
$\gamma(\operatorname{start}(a))=n$ and by definition of matching function
$\operatorname{start}(x,v)\in A_{n}$.

(Step: Item 1b of Figure 2).$(\longleftarrow)$. Let
$\operatorname{end}(a)\not\in M_{n-1}$ be a possible candidate for inclusion
in $I_{n}$. If $\operatorname{start}(a)\in M_{n-1}$ and
$\operatorname{end}(x,v)\in A_{n}$, then $\operatorname{end}(x,v)$ ends the
token started at ${\mu}_{\gamma|^{<n}(\operatorname{start}(a))}$; otherwise,
there would exist ${\mu}_{i}=(A_{i},\delta_{i})$ prior to ${\mu}_{n}$ such
that $\operatorname{end}(x,v)\in A_{i}$, contradicting that $\gamma|^{<n}$ is
undefined on $\operatorname{end}(a)$. By definition of matching function,
since $\operatorname{end}(x,v)\in A_{n}$ ends the token started at
${\mu}_{\gamma(\operatorname{start}(a))}$, we have
$\gamma(\operatorname{end}(a))=n$ and $\operatorname{end}(a)\in I_{n}$.

(Step: Item 1b of Figure 2).$(\longrightarrow)$. If $\operatorname{end}(a)\in
I_{n}$, then by definition of matching function $\operatorname{end}(x,v)\in
A_{n}$. Furthermore, since $\operatorname{end}(a)\in M_{n}$, Item (I) gives
$\gamma(\operatorname{start}(a))\leq\gamma(\operatorname{end}(a))$ for the
atom
$\operatorname{start}(a)\mathrel{\mathsf{\leq}}_{[l,u]}\operatorname{end}(a)$
in $\mathsf{C}$. By definition of event sequence, $\operatorname{start}(x,v)$
and $\operatorname{end}(x,v)$ cannot appear in the same event; hence,
$\gamma(\operatorname{start}(a))<\gamma(\operatorname{end}(a))=n$ and
$\operatorname{start}(a)\in M_{n-1}$.

(Step: Item 2a of Figure 2). Let $T$ be a term in $I_{n}$, and let
$T^{\prime}\in V$ be any other term such that $D_{n-1}[T^{\prime},T]\leq 0$.
Then, $D_{n-1}[T^{\prime},T]$ can either be the lower bound of an atom
$T^{\prime}\mathrel{\mathsf{\leq}}_{[l,u]}T$, or the upper bound of an atom
$T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$ in $\mathsf{C}$. In the first
case, we can directly conclude that $T^{\prime}\in M_{n-1}\cup I_{n}$, because
$T^{\prime}\in M_{n}$ by Item (I) of $\gamma$ and $M_{n}=M_{n-1}\cup I_{n}$ by
definition of $M_{n-1}$ and $I_{n}$. In the second case, note that
$D_{n-1}[T^{\prime},T]=u$, , it has never been decremented because $T\not\in
M_{n-1}$, and that upper bounds $u$ can never be negative. Thus, $u$ is equal
to $0$ and $\gamma$ satisfies
$0\leq\delta({\overline{\mu}}_{[\gamma(T)\ldots\gamma(T^{\prime})]})\leq 0$
(Item (I)), meaning that $\gamma(T^{\prime})=\gamma(T)$ and $T^{\prime}\in
I_{n}$.

(Step: Item 2b of Figure 2). Let $T\in I_{n}$ and $T^{\prime}\in M_{n-1}$.
$D_{n-1}[T^{\prime},T]$ cannot be the upper bound of an atom
$T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$; otherwise, Item (I) would imply
$T\in M_{n-1}$, contradicting $T\in I_{n}$. Thus, $D_{n-1}[T^{\prime},T]$ must
either represent the lower bound of an atom
$T^{\prime}\mathrel{\mathsf{\leq}}_{[l,u]}T$ in $\mathsf{C}$, or be equal to
$+\infty$. In the latter case, $\delta_{n}\geq-D_{n-1}[T^{\prime},T]$
trivially holds. In the former case,
$D_{n-1}[T^{\prime},T]=-l+\delta({\overline{\mu}}_{[\gamma|^{<n}(T^{\prime})\ldots
n-1]})$. Since $\gamma(T)=n$, we have
$\delta({\overline{\mu}}_{[\gamma(T^{\prime})\ldots\gamma(T)]})=\delta({\overline{\mu}}_{[\gamma(T^{\prime})\ldots
n]})=\delta({\overline{\mu}}_{[\gamma(T^{\prime})\ldots n-1]})+\delta_{n}\geq
l$. Hence, $\delta_{n}\geq
l-\delta({\overline{\mu}}_{[\gamma(T^{\prime})\ldots
n-1]})=-D_{n-1}[T^{\prime},T]$.

(Step: Item 2c of Figure 2). Let $T,T^{\prime}\in I_{n}$ be two distinct
terms. Then, $\gamma(T^{\prime})=\gamma(T)$ and
$\delta({\overline{\mu}}_{[\gamma(T^{\prime})\ldots\gamma(T)]})=0$. If
$T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$ (resp.,
$T^{\prime}\mathrel{\mathsf{\leq}}_{[l,u]}T$) belongs to $\mathsf{C}$, then
$D_{n-1}[T,T^{\prime}]$ (resp., $D_{n-1}[T^{\prime},T]$) is the lower bound
$l$ and equals 0 by Item (I). Otherwise,
$D_{n-1}[T,T^{\prime}]=D_{n-1}[T^{\prime},T]=+\infty$.

Hence,
$\mathsf{M}_{n-1}\mathrel{\xlongrightarrow{{\mu}_{n},{I}_{n}}}\mathsf{M}_{n}$
is well defined and $\langle I_{1},\ldots,I_{n}\rangle$ is a run of
$\mathsf{M}_{\mathsf{E}}$ on ${\overline{\mu}}$ yielding $\mathsf{M}_{n}$.

$(\longrightarrow)$. We proceed by induction on the length of the event
sequence ${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$.

Base case:

An empty run ${\overline{}{I}}$ yields
$\mathsf{M}_{\mathsf{E}}=(V,D,\varnothing,0)$ itself. Then the function
$\gamma_{0}:\varnothing\to\varnothing$ vacuously satisfies the definition of
matching function and Items (I) and (II).

Inductive step:

Let ${\overline{}{I}}=\langle I_{1},\ldots,I_{n}\rangle$ be a run of
$\mathsf{M}_{\mathsf{E}}$ on ${\overline{\mu}}$, yielding a matching structure
$\mathsf{M}_{n}=(V,D_{n},M_{n},t_{n})$. Note that ${\overline{}{I}}_{[1\ldots
n-1]}$ is a run of $\mathsf{M}_{\mathsf{E}}$ on ${\overline{\mu}}_{[1\ldots
n-1]}$ yielding a matching structure
$\mathsf{M}_{n-1}=(V,D_{n-1},M_{n-1},t_{n-1})$. By the inductive hypothesis,
there exists a matching function $\gamma_{<n}:M_{n-1}\to[1,\ldots,n-1]$
satisfying Items (I) and (II). Let $\gamma:M_{n}\to[1,\ldots,n]$ be the
extension of $\gamma_{<n}$ to $M_{n}$, such that $\gamma(T)=n$, for all $T\in
I_{n}$.

(Step: $\gamma$ is a matching function). Items 1 and 2 hold for all the terms
already present in the domain of $\gamma_{<n}$. For every term in $I_{n}$,
Item 1 for $\gamma$ follows from Item 1 of $I_{n}$-match event. Let
$\operatorname{start}(a),\operatorname{end}(a)\in M_{n}$ be two terms not both
already present in $M_{n-1}$, meaning that $\operatorname{start}(a)\in
M_{n-1}$ and $\operatorname{end}(a)\in I_{n}$, for some quantified token
$a[x=v]$ in $\mathsf{E}$. By definition of $I_{n}$-match event,
${\mu}_{n}=(A_{n},\delta_{n})$ is such that $\operatorname{end}(x,v)\in A_{n}$
and no other event in ${\mu}_{[\gamma_{<n}(T)\ldots n-1]}$ contains an action
$\operatorname{end}(x,v)$, otherwise $\operatorname{end}(a)$ would already
belong to $M_{n-1}$ (by Item 1b of $I$-match event). Thus,
$\operatorname{end}(x,v)\in A_{n}$ ends the token started at
${\mu}_{\gamma(\operatorname{start}(a))}$, and
$\gamma(\operatorname{start}(a))$ and $\gamma(\operatorname{end}(a))$
correctly identify the endpoints of such token.

(Step: Item (I) of Lemma 2). Let $T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$
be an atom in $\mathsf{C}$, and note that $\gamma$ already satisfies Item (I)
for every $T^{\prime}\in M_{n-1}$. If $T^{\prime}\in I_{n}$ instead, consider
the entry $D_{n-1}[T,T^{\prime}]$ representing the lower bound $l$ of the
aforementioned atom. If $D_{n-1}[T,T^{\prime}]\leq 0$, Item 2a of $I$-match
event gives $T\in M_{n-1}\cup I_{n}=M_{n}$. If $D_{n-1}[T,T^{\prime}]>0$,
$D_{n-1}[T,T^{\prime}]$ no longer stores its initial value $-l\leq 0$, meaning
that $T$ must have been previously matched and $T\in M_{n-1}\subseteq M_{n}$.
In either case, $T\in M_{n}$ and $\gamma(T)\leq\gamma(T^{\prime})$, because
$\gamma(T)\leq n$. If $T\in I_{n}$, then
$\delta({\overline{\mu}}_{[\gamma(T)\ldots\gamma(T^{\prime})]})=0\leq u$, is
trivially satisfied by any upper bound $u$. Furthermore, by Item 2c of
$I$-match event, either the lower bound $D_{n-1}[T,T^{\prime}]=0$ or the upper
bound $D_{n-1}[T^{\prime},T]=0$, and they both equal their initial values $l$
and $u$. Note that the former case is also implied by the latter, so that
$l=0$ and
$l\leq\delta({\overline{\mu}}_{[\gamma(T)\ldots\gamma(T^{\prime})]})$. If
$T\in M_{n-1}$, by Item 2b of $I$-match event,
$\delta_{n}\geq-D[T,T^{\prime}]=l-\delta({\overline{\mu}}_{[\gamma(T)\ldots
n-1]})$. Hence, $l\leq\delta({\overline{\mu}}_{[\gamma(T)\ldots
n-1]})+\delta_{n}=\delta({\overline{\mu}}_{[\gamma(T)\ldots\gamma(T^{\prime})]})$.
While $\delta_{n}\leq
D_{n-1}[T^{\prime},T]=u-\delta({\overline{\mu}}_{[\gamma(T)\ldots n-1]})$,
since ${\mu}_{n}$ is an admissible event for $\mathsf{M}_{n-1}$. Hence,
$\delta({\overline{\mu}}_{[\gamma(T)\ldots
n-1]})+\delta_{n}=\delta({\overline{\mu}}_{[\gamma(T)\ldots\gamma(T^{\prime})]})\leq
u$.

(Step: Item (II) of Lemma 2). Let $T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$
be an atom in $\mathsf{C}$ such that $T\in M_{n}$ and $T^{\prime}\not\in
M_{n}$. Since ${\mu}_{n}$ is an admissible event for $\mathsf{M}_{n-1}$,
$\delta_{n}\leq
D_{n-1}[T^{\prime},T]=u-\delta({\overline{\mu}}_{[\gamma(T)\ldots n-1]})$.
Hence, $\delta({\overline{\mu}}_{[\gamma(T)\ldots
n-1]})+\delta_{n}=\delta({\overline{\mu}}_{[\gamma(T)\ldots n]})\leq u$.

See 3

######  Proof 7.2.

Let
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma_{r}}\mathsf{M}_{r}=(V,D_{r},M_{r},t_{r})$
and
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma_{s}}\mathsf{M}_{s}=(V,D_{s},M_{s},T_{s})$,
with
$\gamma_{s}(\operatorname{start}(a_{0}))\leq\gamma_{r}(\operatorname{start}(a_{0}))$.
Let $M=M_{r}\cup M_{s}$ and $\gamma:M\to[1,\ldots,n]$ be a function defined
as:

$\gamma(T)=\begin{cases}\gamma_{s}(T)&\text{if }T\in M_{s}\cap M_{r}\text{ and
}\gamma_{s}(T)\leq\gamma_{r}(T)\\\ \gamma_{r}(T)&\text{if }T\in M_{s}\cap
M_{r}\text{ and }\gamma_{s}(T)>\gamma_{r}(T)\\\ \gamma_{s}(T)&\text{if }T\in
M_{s}\setminus M_{r}\\\ \gamma_{r}(T)&\text{if }T\in M_{r}\setminus
M_{s}\end{cases}$

(Step: $\gamma$ is a matching function). Item 1 of Section 3.1 for $\gamma$
follows from our hypothesis on $\gamma_{s}$ and $\gamma_{r}$. Regarding Item
2, let $\operatorname{start}(a),\operatorname{end}(a)\in M$ for some
quantified token $a[x=v]$ in $\mathsf{E}$. If $\gamma_{s}$ and $\gamma_{r}$
map the endpoints of $a$ to the same token in ${\overline{\mu}}$, then
$\gamma(\operatorname{start}(a))$ and $\gamma(\operatorname{end}(a))$
correctly identify the endpoints of that token. If instead $\gamma_{s}$ and
$\gamma_{r}$ map $a$ to two distinct tokens in ${\overline{\mu}}$, then
$\gamma$ would match $a$ according to the function whose token comes first,
correctly identifying the endpoints of such token.

(Step: $\gamma$ satisfies Items (I) and (II) of Lemma 2). Let
$T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$ be an atom in $\mathsf{C}$. If
$T^{\prime}\in M$, then either $T^{\prime}\in M_{s}$, and $T\in M_{s}\subseteq
M$, or $T^{\prime}\in M_{r}$, and $T\in M_{r}\subseteq M$. If $\gamma$ maps
both terms with either $\gamma_{s}$ or $\gamma_{r}$, then
$\gamma(T)\leq\gamma(T^{\prime})$ and
$l\leq\delta({\overline{\mu}}_{[\gamma(T)\ldots\gamma(T^{\prime})]})\leq u$
immediately follows. If instead $\gamma(T)=\gamma_{s}(T)$ and
$\gamma(T^{\prime})=\gamma_{r}(T^{\prime})$, then $T^{\prime}\in M_{r}$ and
$T\in M_{s}\cap M_{r}$. By definition of $\gamma$,
$\gamma_{s}(T)\leq\gamma_{r}(T)$, and, by Item (I) for $\gamma_{r}$,
$\gamma_{r}(T)\leq\gamma_{r}(T^{\prime})$. Hence,
$\gamma(T)\leq\gamma(T^{\prime})$. If $T^{\prime}\in M_{s}$, then
$\gamma_{s}(T^{\prime})>\gamma_{r}(T^{\prime})$, and:

$\displaystyle l$
$\displaystyle\leq\delta_{\gamma_{r}(T),\gamma_{r}(T^{\prime})}$
$\displaystyle\text{\lx@cref{creftypecap~refnum}{lemma:function-matching-
run:entire-atom} for }\gamma_{r}$
$\displaystyle\leq\delta_{\gamma_{s}(T),\gamma_{r}(T^{\prime})}$
$\displaystyle\text{}\gamma_{s}(T)\leq\gamma_{r}(T)$
$\displaystyle<\delta_{\gamma_{s}(T),\gamma_{s}(T^{\prime})}$
$\displaystyle\text{}\gamma_{s}(T^{\prime})>\gamma_{r}(T^{\prime})$
$\displaystyle\leq u$
$\displaystyle\text{\lx@cref{creftypecap~refnum}{lemma:function-matching-
run:entire-atom} for }\gamma_{s}$

otherwise:

$\displaystyle l$
$\displaystyle\leq\delta_{\gamma_{r}(T),\gamma_{r}(T^{\prime})}$
$\displaystyle\text{\lx@cref{creftypecap~refnum}{lemma:function-matching-
run:entire-atom} for }\gamma_{r}$
$\displaystyle<\delta_{\gamma_{s}(T),\gamma_{r}(T^{\prime})}$
$\displaystyle\text{}\gamma_{s}(T)\leq\gamma_{r}(T)$
$\displaystyle\leq\delta_{\gamma_{s}(T),n}$
$\displaystyle\text{}\gamma_{r}(T^{\prime})\leq n$ $\displaystyle\leq u$
$\displaystyle\text{\lx@cref{creftypecap~refnum}{lemma:function-matching-
run:partial-atom} for }\gamma_{s}$

The case for $\gamma(T)=\gamma_{r}(T)$ and
$\gamma(T^{\prime})=\gamma_{s}(T^{\prime})$ is completely symmetrical.

Lastly, if $T^{\prime}\not\in M$, but $T\in M$, then either
$\gamma(T)=\gamma_{s}(T)$ or $\gamma(T)=\gamma_{r}(T)$, and Item (II) for
$\gamma$ follows from Item (II) for $\gamma_{s}$ and $\gamma_{r}$.

See 4

######  Proof 7.3.

Let $\gamma(\operatorname{start}(a_{0}))=s$, assuming there is no residual
matching structure $\mathsf{M}_{k}$ in the sequence
$\langle\mathsf{M}_{s},\ldots,\mathsf{M}_{n-1}\rangle$, then for every
matching structure $\mathsf{M}_{i}=(V,D_{i},M_{i},t_{i})$, where $s\leq i<n$,
there exists a pair of terms $(T,T^{\prime})$ such that $T\in M_{i}$ and
$T^{\prime}\not\in M_{i}$, and their distance $D_{i}[T^{\prime},T]$ has a
finite upper bound. Let $E\subseteq V\times V$ be the set that collects all
pairs $(T,T^{\prime})$ for the matching structures $\mathsf{M}_{i}$. We define
$\delta_{T,T^{\prime}}$ as
$\delta({\overline{\mu}}_{[\gamma(T)\ldots\gamma(T^{\prime})]})$ if
$\gamma(T^{\prime})$ is defined, or as
$\delta({\overline{\mu}}_{[\gamma(T)\ldots n]})$ otherwise. Let
$\delta_{E}=\sum_{(T,T^{\prime})\in E}\delta_{T,T^{\prime}}$ and note that
$\delta_{E}\geq\delta({\overline{\mu}}_{[\gamma(\operatorname{start}(a_{0}))\ldots
n]})$, because every position in
${\overline{\mu}}_{[\gamma(\operatorname{start}(a_{0}))\ldots n]}$ is covered
by some distance $\delta_{T,T^{\prime}}$. Moreover, each pair
$(T,T^{\prime})\in E$ corresponds to an atom of the form
$T\mathrel{\mathsf{\leq}}_{[l,u]}T^{\prime}$ in $\mathsf{C}$. According to
Lemma 2, we have $\delta_{T,T^{\prime}}\leq u$, and therefore,
$\delta_{E}\leq\operatorname{window}(P)$. Hence, we have
$\delta({\overline{\mu}}_{[\gamma(\operatorname{start}(a_{0}))\ldots
n]})\leq\delta_{E}\leq\operatorname{window}(P)$: a contradiction hence proving
the existence of a residual matching structure $M_{k}$.

See 5

######  Proof 7.4.

$(\longrightarrow)$. Let
${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ be a solution plan
for $P$, and let ${\overline{q}}=\langle q_{0},\ldots,q_{n}\rangle$ be the run
of $\mathsf{A}_{P}$ on ${\overline{\mu}}$. We first show that the sink state
is never reached, and then that $q_{n}$ is a final state.

Let ${\mu}_{s}=(A_{s},\delta_{s})$ be the trigger event of a rule
$\mathsf{R}\equiv
a_{0}[x_{0}=v_{0}]\rightarrow\mathsf{E}_{1}\lor\dots\lor\mathsf{E}_{m}$, ,
$\operatorname{start}(x_{0},v_{0})\in A_{s}$. Since ${\overline{\mu}}$ is a
solution plan, there exist tokens satisfying an existential statement
$\mathsf{E}$ of $\mathsf{R}$ for the trigger ${\mu}_{s}$. Hence, by Lemmas 2
and 1 there exists a run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma}\mathsf{M}_{n}$,
yielding a _closed_ matching structure $\mathsf{M}_{n}$, such that
$\gamma(\operatorname{start}(a_{0}))=s$.

Let
$\overline{\mathsf{M}}=\langle\mathsf{M}_{\mathsf{E}},\mathsf{M}_{1},\ldots,\mathsf{M}_{n}\rangle$
be the sequence of all the matching structures involved in such run. Note
that, by construction (Section 4.3), the states of ${\overline{q}}$ induce all
the possible runs for the _initial_ matching structures of $P$ that can be
defined on ${\overline{\mu}}$. In particular, the run $\gamma$ must be one of
them. However, only a subsequence of the matching structures $\overline{M}$
will appear in the states of the run ${\overline{q}}$. Indeed, we can identify
three key points for the sequence $\overline{M}$: the least position $s$ such
that $\mathsf{M}_{s}$ is _active_ (corresponding to
$\gamma(\operatorname{start}(a_{0}))$), the least position $h$ following $s$
such that $\mathsf{M}_{h}$ no longer belongs to the component $\Upsilon$ of
the states in ${\overline{q}}_{[h\ldots n]}$, either because $\mathsf{M}_{h}$
is _closed_ or because $\delta({\overline{\mu}}_{[s\ldots
h]})>\operatorname{window}(P)$, and the least position $k$ following $h$ such
that $\mathsf{M}_{k}$ no longer belongs to the component $\Delta$ of the
states in ${\overline{q}}_{[k\ldots n]}$, either because $\mathsf{M}_{k}$ is
_closed_ or because it gets discarded in favour of the matching structures of
a later trigger event.

Every matching structure in $\overline{M}_{[1\ldots h-1]}$ belongs to the
component $\Upsilon$ of a corresponding state in ${\overline{q}}_{[1\ldots
h-1]}$, so the set $\Upsilon$ of the state $q_{s-1}$ is such that
$\mathsf{M}_{s}\in$, satisfying condition 5b of Section 4.3 for the trigger
event ${\mu}_{s}$. Matching structures $\overline{M}_{[s+1\ldots h]}$ instead
belong to the set , for the partition $\Upsilon^{\mathsf{R}}_{t}$ tracking the
satisfaction of the trigger event ${\mu}_{s}$ of every state
${\overline{q}}_{[s\ldots h-1]}$. Hence, all such states satisfy condition 5a
of Section 4.3.

We now show that no _active_ matching structures for the trigger event
${\mu}_{s}$ exists after some state $q_{h}$, following $q_{s}$ in
${\overline{q}}$. Note that the run $\gamma$ yields a _closed_ matching
structure, and if it does so within $\operatorname{window}(P)$ time units from
the event ${\mu}_{\operatorname{start}(a_{0})}$, we identified such position
as the closed matching structure $\mathsf{M}_{h}$. So that the state $q_{h-1}$
is such that $\mathsf{M}_{h}\in$, for the partition
$\Upsilon^{\mathsf{R}}_{t}$ tracking the trigger event ${\mu}_{s}$, and is
discarded from $q_{h}$.

If instead $\gamma$ yields a _closed_ matching structure after
$\operatorname{window}(P)$ time units from the event
${\mu}_{\operatorname{start}(a_{0})}$, lets identify such position as
$\mathsf{M}_{j}$, with $j\leq n$. If $\mathsf{M}_{j-1}$ belongs to the set
$\Delta(\mathsf{E})$ of the state $q_{j-1}$, then $\mathsf{M}_{j}\in$, so that
is _closed_ and discarded from $q_{j}$, alongside all the other matching
structures in $\Delta(\mathsf{E}^{\prime})$, for every
$E^{\prime}\in\Phi(\mathsf{E})$, , for every other existential statement
$\mathsf{E}^{\prime}$ of $\mathsf{R}$ still tracking the trigger ${\mu}_{s}$.
If instead $\mathsf{M}_{j-1}$ for the trigger event ${\mu}_{s}$ does not
belong to the set $\Delta(\mathsf{E})$ of the state $q_{j-1}$, by construction
(Section 4.3), there exist a state $q_{h}$ in which the matching structures
tracking ${\mu}_{s}$ have been replaced by those of a later event, and they no
longer appear in $\Delta(\mathsf{E})$ from $q_{h}$ onwards.

Since ${\overline{\mu}}$ is a solution plan, the previous argument holds for
all the trigger events in ${\overline{\mu}}$ of any rules in $S$. Hence,
conditions 5b and 5a are always met, , the sink state is never reached, and no
active matching structures belong to $q_{n}$, making it a final state.

$(\longleftarrow)$. Let
${\overline{\mu}}=\langle{\mu}_{1},\ldots,{\mu}_{n}\rangle$ be an event
sequence accepted by $\mathsf{A}_{P}$ and let $\rho=\langle
q_{0},\ldots,q_{n}\rangle$ be its accepting run. We have to show that the plan
corresponding to ${\overline{\mu}}$ is a solution plan for $P$, , for every
event triggering a rule $\mathsf{R}$ in $S$, at least one of the existential
statements of $\mathsf{R}$ is satisfied by ${\overline{\mu}}$.

Let ${\mu}_{s}=(A_{s},\delta_{s})$ be an event in ${\overline{\mu}}$
triggering a rule $\mathsf{R}\equiv
a_{0}[x_{0}=v_{0}]\rightarrow\mathsf{E}_{1}\lor\dots\lor\mathsf{E}_{m}$, ,
$\operatorname{start}(x_{0},v_{0})\in A_{s}$. Since the sink state is never
visited in an accepting run, the state $q_{s}$, reached upon reading the event
${\mu}_{s}$, is such that the partition $\Upsilon^{\mathsf{R}}_{0}$, tracking
the satisfaction of the trigger event ${\mu}_{s}$, is not empty. For the same
reason, the partition $\Upsilon^{\mathsf{R}}_{t}$ tracking ${\mu}_{s}$ in
every state following $q_{s}$ can never be empty as a result of the function .
However, since the final state $q_{n}$ does not contain any _active_ matching
structure, there must exists a state $q_{h}$ in ${\overline{q}}$ whose
partition gets discarded from $q_{h+1}$. This can happen either because is a
_closed_ set, or because the matchings structures in get promoted to the
component $\Delta$. In the first case, we can conclude that there exists a run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma}\mathsf{M}_{n}$
for the initial matching structure $\mathsf{M}_{\mathsf{E}}$ of an existential
statement $\mathsf{E}$ of $\mathsf{R}$ such that $\mathsf{M}_{n}$ is _closed_
and $\gamma(\operatorname{start}(a_{0}))=s$, hence, by Observations 1 and 2,
the trigger event ${\mu}_{s}$ satisfies $\mathsf{R}$.

In the second case, let $\Psi$ be the set of existential statements having an
active matching structure in , so that we can identify them as the sets
$\Delta(\mathsf{E})$, for $\mathsf{E}\in\Psi$, in the states from $q_{h+1}$
onwards. By Lemma 4, every such set contains a _residual_ matching structure.
Hence, by Observation 2, they can become empty only if, at some state $q_{k}$
following $q_{h}$, contains a _closed_ matching structure for some existential
statement $\mathsf{E}\in\Psi$. Note that the run ${\overline{q}}$ is an
accepting run, so every non-empty set $\Delta(\mathsf{E})$ must become empty
before the end of the run. Hence, $q_{k}$ is guaranteed to exist.

However, it may be the case that, by the time is _closed_ ,
$\Delta(\mathsf{E})$ no longer contains the matching structures for the
trigger event ${\mu}_{s}$, but those for a later trigger event ${\mu}_{r}$ of
$\mathsf{R}$. Since the sets $\Delta(\mathsf{E})$ store only the matching
structures tracking the most recent trigger event older than
$\operatorname{window}(P)$. Thus, if contains a _closed_ matching structure
for ${\mu}_{s}$, we can directly assert the existence of a run for
$\mathsf{M}_{\mathsf{E}}$ implying the satisfaction of $\mathsf{R}$ for the
trigger event ${\mu}_{s}$. If instead contains a _closed_ matching structure
$\mathsf{M}_{r}$ for a later event ${\mu}_{r}$, there exists a run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma_{r}}\mathsf{M}_{r}$,
such that $\gamma_{r}(\operatorname{start}(a_{0}))=r$. Furthermore, by a
previous consideration on $q_{h+1}$, there exists a run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}}_{[1\ldots
h+1]},\gamma_{s}}\hat{}\mathsf{M}_{h+1}$, yielding a _residual_ matching
structure $\hat{}\mathsf{M}_{h+1}$, and, by Observation 2, such run can be
extended on the entire event sequence
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma_{s}}\hat{}\mathsf{M}_{n}$,
to yield a _residual_ matching structure $\hat{}\mathsf{M}_{n}$. Given
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma_{r}}\mathsf{M}_{r}$
and
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma_{s}}\hat{}\mathsf{M}_{n}$,
with
$\gamma_{s}(\operatorname{start}(a_{0}))\leq\gamma_{r}(\operatorname{start}(a_{0}))$,
by Lemma 3, there exists a run
$\mathsf{M}_{\mathsf{E}}\xlongrightarrow{{\overline{\mu}},\gamma_{s}}\mathsf{M}_{n}$
yielding a matching structure $\mathsf{M}_{n}$ matching as many terms as
$\mathsf{M}_{r}$ and such that $\gamma_{s}(\operatorname{start}(a_{0}))=s$.
Hence, $\mathsf{M}$ is a _closed_ matching structure for the existential
statement $\mathsf{E}$, and, by Observations 1 and 2, $\mathsf{R}$ satisfies
the trigger event ${\mu}_{s}$.

Furthermore, all the value duration functions are satisfied by the tokens in
${\overline{\mu}}$, being encoded as synchronisation rules by the automaton
$S_{P}$. Meanwhile, the automaton $T_{P}$ guarantees the fulfilment of the
value transition functions. Hence, we can conclude that ${\overline{\mu}}$ is
a solution plan for $P$, because every rule in $S$ is satisfied, as well as
the value duration and value transition functions of every state variable.