{'fraction_non_alphanumeric': 0.0595115881163478, 'fraction_numerical': 0.00973712863586872, 'mean_word_length': 3.7017697820681588, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 25, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Dynamic Controllability of Conditional Simple Temporal Networks is PSPACE-complete

Even after the proposal of various solution algorithms, the precise computational complexity of checking whether a Conditional Temporal Network is Dynamically Controllable had still remained widely open. This issue gets settled in this paper which provides constructions, algorithms, and bridging lemmas and arguments to formally prove that: (1) the problem is PSPACE-hard, and (2) the problem lies in PSPACE.


I. INTRODUCTION
In temporal planning and scheduling, a Simple Temporal Network (STN) [1] consists of a set of tasks to be scheduled on the time line, and a set of constraints of the form Y −X ≤ δ, with δ ∈ R, i.e., limiting the difference between the execution times of tasks X and Y . The STN is said to be consistent if it admits a schedule of its tasks that satisfies all the constraints. Some variants of the STN model have been proposed in the literature to allow and represent some forms of contingency, that is, the presence of parameters which are unknown to the planner. For example, a Conditional Simple Temporal Network (CSTN) [2] comprises also a set of unknown propositional variables, and some of the tasks and constraints in the network are to be taken into account only for specific values of these variables.
When contingency is present, such as in CSTNs, the notion of consistency is replaced by the notion of controllability, which comes in three flavors: weak, strong, and dynamic [3], [2]. In all the three variants the question is whether the planner is able to provide a schedule that satisfies the constraints; the difference is in how and when the value of the unknown parameters is disclosed to the planner. In the weak controllability, the parameters are revealed before the execution of the plan, so the schedule can be decided once the value of all the variables (scenario) has been specified, and the main question is deciding whether a feasible scheduling exists for all possible scenarios. In the strong controllability, these values are revealed only after the execution of the schedule, so we need a single schedule that works for every scenario. In the dynamic controllability, the unknown parameters are revealed progressively during the execution of the plan, as a consequence of actions performed by the planner. In the case of CSTNs, each propositional variable is associated with an observation task, and its value is revealed precisely when the corresponding observation task is executed. Here we look for a dynamic execution strategy: a schedule of the tasks that gets dynamically decided depending on the partial scenario progressively observed, such that, whatever scenario possibly emerges, all the constraints pertinent to that scenario will be respected. The dynamic controllability 1 decision problem for CSTNs (CSTN-DC) asks to check whether a given CSTN is dynamically controllable, and is a major algorithmic problem associated to CSTNs.
It is known that the consistency of STNs can be decided in polynomial time, by interpreting the network as a weighted graph and applying the Floyd-Warshall All-Pairs Shortest Path algorithm [1]. However, the presence of contingency might change drastically the algorithmic nature of the problem. Especially for the dynamic controllability, which introduces an alternation of quantifiers ∃ (for the choices of the planner) and ∀ (for the revealed parameters), an increase in complexity is expected [3]. In the case of Simple Temporal Networks with Uncertainty (STNUs), another variant of STNs with contingency (with which a first controllability issue was posed), the dynamic controllability had been conjectured to be PSPACE-complete [3]. Subsequently, it was proven to actually lie in P [4].
For CSTNs, determining the right complexity class of dynamic controllability is still a widely open question. Deciding their weak controllability has been proven to be coNP-complete [2], [5] and, since weak controllability can easily be reduced to a special case of dynamic controllability, then CSTN-DC is at least coNP-hard [5]. A first complete algorithmic solution had been proposed in [6] by reducing CSTN-DC to a time automaton game of high complexity. Later, a complete constraint propagation algorithm was achieved with much better performances in practice [7], based on the sound constraint-propagation rules provided in [8], [9], [10] for the more general setting of Conditional Simple Temporal Networks with Uncertainty (CSTNU). In [5], a worst-case upper bound is obtained, thanks to an algorithm which requires singly-exponential time and memory. To the best of our knowledge, no better bounds are known in the literature.
In this work, we settle this question by sharply improving both the lower and the upper bound. After providing the background notions and first basic facts as common to both developments in Section II, a reduction from Quantified 3-SAT to CSTN-DC is proposed in Section III, which proves the latter to be PSPACE-hard. Then, in Section IV, the first algorithm that solves CSTN-DC using only polynomial memory is given, hence showing that CSTN-DC lies in PSPACE. Sections III and IV can be read independently. Taken together, their negative and positive results show that CSTN-DC is PSPACE-complete, i.e., the natural complexity class for the dynamic controllability issue for CSTNs is PSPACE.

II. BACKGROUND
In this section, Conditional Simple Temporal Networks (CSTNs) and their dynamic controllability are formally defined. The definitions are taken from [7].

A. Simple Temporal Networks (STNs)
Definition 1 (Temporal variables, tasks, constraints). Let T be a finite set of real-valued temporal variables. Each variable X ∈ T represents the execution time of a task, also denoted with X. In the following, we use the terms temporal variable and task interchangeably. A binary difference constraint over T is a constraint of the form Y − X ≤ δ, for X, Y ∈ T and δ ∈ R. In this paper, constraint always denotes a binary difference constraint. The constraint Y − X ≤ δ can also be expressed, equivalently, as X − Y ≥ −δ, Y ≤ X + δ or X ≥ Y − δ, as it is more convenient in the context. Definition 2 (Schedule, satisfied constraints). A schedule over T is a total assignment ψ : T → R of the temporal variables in T . We write [ψ] X instead of ψ(X) to denote the value assigned by the schedule ψ to the variable Definition 3 (Simple Temporal Network). A Simple Temporal Network (STN) is a pair (T , C) where T is a set of temporal variables and C is a set of constraints over T .
Definition 4 (Feasible schedule). A schedule ψ over T is feasible for (T , C) if ψ satisfies all the constraints in C.

B. Conditional Simple Temporal Networks (CSTNs)
Definition 5 (Propositional variables, labels). Let P be a set of propositional (boolean) variables. A label over P is a boolean formula = l 1 ∧ · · · ∧ l k , obtained as conjunction of positive or negative literals l i ∈ {p i , ¬p i } on distinct variables p i ∈ P. The empty label is denoted with λ and always evaluates to true. Let P * denote the set of labels over P (including λ).
Definition 6 (Scenario, label evaluation). A scenario s over P is a total assignment of the propositional variables s : P → {0, 1} where 0 means false and 1 means true. Let Σ P denote the set of all the scenarios over P. We write s if the label evaluates to true under the interpretation given by s.
where Y − X ≤ δ is a constraint over T and ∈ P * is a label, • L : T → P * if a function that assigns a label L(X) to each task X ∈ T , • OT ⊆ T is the set of observation tasks, • O : P → OT is a bijection that associates each propositional variable p ∈ P to a unique observation task O(p).
A task X ∈ T has to be executed only in those scenarios s ∈ Σ P such that s L(X), and each constraint (Y − X ≤ δ, ) ∈ C has to be satisfied if s . Since the constraint Y − X ≤ δ only makes sense if both X and Y get executed, we require the following well-definedness property.
In the following, WD1 is incorporated in the definition of CSTN, i.e., it is assumed that any CSTN satisfies this restriction. Remark 1. Tsamardinos et al. [2] discussed some supplementary reasonability assumptions that any well-defined CSTN must satisfy. Subsequently, those conditions have been analyzed and formalized in [8] introducing the three restrictions WD1, WD2, and WD3. The restriction WD1 has already been discussed. The restrictions WD2 and WD3 relate the labels on tasks and constraints with the labels on observation tasks. We avoid entering into the fine details regarding them, and we rather provide both of our results in their strongest and most general form, as follows. First, the reduction in our PSPACE-hardness proof constructs only CSTNs that comply with all three restrictions vacuously, having no labels on the tasks. Second, neither WD2 nor WD3 are required as preconditions for the applicability of our PSPACE algorithm. 2 C. Dynamic controllability of CSTNs Definition 9 (Projection). The projection of a CSTN over a scenario s is the STN Γ s = (T s , C s ) where: Definition 10 (Execution strategy, viable). Let Ψ T denote the set of schedules ψ over any subset T ⊆ T . For a schedule ψ ∈ Ψ T over T ⊆ T , let Dom(ψ) = T . An execution strategy for Γ is a function σ : Σ P → Ψ T that maps each scenario s ∈ Σ P to a schedule σ(s) for Γ s (i.e. Dom(σ(s)) = T s ). An execution strategy σ is viable if, for every scenario s ∈ Σ P , the schedule σ(s) is feasible for Γ s .
Definition 11 (Partial scenario, history). A partial scenario over P is a partial assignment h : Dom(h) → {0, 1} of the propositional variables, where Dom(h) ⊆ P. Given σ, a scenario s, and a time point t ∈ R, the history at t in the scenario s with the strategy σ is the partial scenario Hist(t, s, σ) where Dom(Hist(t, s, σ)) = {p ∈ P | [σ(s)] O(p) < t} and Hist(t, s, σ)(p) = s(p) for every p ∈ Dom(Hist(t, s, σ)).
Definition 13 (Dynamic controllability). A CSTN is dynamically controllable if it admits a dynamic viable execution strategy. The dynamic controllability decision problem (CSTN-DC) asks to check whether a given CSTN Γ is dynamically controllable or not.
The following definition and lemma state a useful characterization of dynamic execution strategies: if two scenarios differ in only one propositional variable, then a dynamic execution strategy behaves in the same way in the two scenarios until that propositional variable is observed. This property has been also proven in [7, Theorem 1], and will be used several times in this paper to exploit the fact that an execution strategy is dynamic.
Definition 14. Given a scenario s ∈ Σ P , a propositional variable p ∈ P and v ∈ {0, 1}, let s[v/p] be the scenario obtained from s by changing the value of the variable p to v, i.e., s[v/p](p) = v and s[v/p](q) = s(q) for q ∈ P \ {p}. Lemma 1. Let σ be a dynamic execution strategy. Let s ∈ Σ P , p ∈ P, v ∈ {0, 1}, and consider the scenario Proof: Observe that we only need to check the properties for those values of t that appear somewhere in σ. Hence, we can proceed by induction. The properties clearly hold for a sufficiently small t (less than any value in σ). Take ∈ (t, t ) for every X ∈ T , and assume that the properties hold for t. Observe that, for s ∈ {s, s }, Dom(Hist(t , s , σ)) = Dom( Hence, Hist(t , s, σ) = Hist(t , s , σ). The other two properties for t are a direct consequence of the fact that σ is dynamic, and this concludes the induction.

III. PSPACE-HARDNESS
In this section, we prove that CSTN-DC is PSPACE-hard by showing a reduction from Quantified 3-SAT (Q3SAT).
We are given a Q3SAT formula Φ = ∃x 1 ∀y 1 · · · ∃x n ∀y n ϕ where ϕ is a 3CNF over the propositional variables x 1 , y 1 , . . . , x n , y n . I.e., ϕ = m j=1 (l j,1 ∨ l j,2 ∨ l j,3 ) and each literal l j,k is either a positive or a negated occurrence of one of the quantified variables. The formula Φ can be understood as a game in which the existential player and the universal player decide in turn the value of the variables x 1 , y 1 , x 2 , y 2 , . . . , x n , y n . The existential players wins if, when all the variables have been set, the formula ϕ is satisfied by the chosen values. CSTNs can be also seen as games, where the planner plays against the nature, the first by scheduling the tasks, the second by choosing the value of the propositional variables as soon as they are observed. The planner wins if, eventually, the schedule he executes is feasible, and the CSTN is dynamically controllable if the planner has a winning strategy. This interpretation of both Q3SAT and CSTN-DC as two-player games underlies our proof of PSPACE-hardness.
We will describe a CSTN Γ Φ which is dynamically controllable iff Φ ≡ true, that is, iff the existential player has a winning strategy for Φ. It will be apparent that O(log(n + m)) internal space suffices in order to construct Γ Φ out from Φ.

A. Warm-up: the controller can choose some variables
Before addressing CSTN-DC, we consider a more general problem CSTN + -DC. We define a CSTN + to be a CSTN in which the values of a subset P + ⊆ P of the propositional variables are actually decided by the controller rather than by the nature, still each p ∈ P gets determined at the precise execution time of the corresponding disclosure task O(p). To ease our exposition, we first construct a CSTN + Γ + Φ which is dynamically controllable iff Φ ≡ true. This will be a much easier task, but helps in delivering the general idea of the reduction.
The CSTN + Γ + Φ contains all the variables x i , y i as propositional variables, decided and observed respectively in tasks . These constraints connect the tasks X 1 , Y 1 , . . . , X n , Y n in a chain which enforces that they are executed in the proper order. Then, we have two tasks A and B with the following constraints. For every j = 1, . . . , m, we have a constraint B ≥ A + 1 with label j := ¬l j,1 ∧ ¬l j,2 ∧ ¬l j,3 , defined as the negation of the j-th The network Γ + Φ is dynamically controllable iff Φ ≡ true. Indeed, if Φ ≡ true, the controller schedules X i and Y i at time 2i and 2i + 1 respectively, and can choose the propositional value of x i depending on y 1 , . . . , y i−1 in accordance to his winning strategy for Φ. Finally, he schedules B at time 2n + 2 and A at time 2n + 3, and, since every clause of ϕ is satisfied, none of the constraints B ≥ A + 1 applies and all the other constraints are fulfilled. Conversely, assume Φ ≡ false. It is now nature that owns a winning strategy: since the controller is anyhow forced to reveal the variables in order, she can choose each propositional variable y i depending on x 1 , . . . , x i so that, for at least one j ∈ {1, . . . , m}, the clause (l j,1 ∨ l j,2 ∨ l j,3 ) evaluates to false. Hence, the constraints A ≥ B + 1 and B ≥ A + 1 necessarily lead to a conflict, no matter when the events A and B are scheduled.

B. Reduction for CSTNs
The above toy reduction with Γ + Φ illustrates well the general framework, but relies on the strong assumption that the controller can choose the value of some of the propositional variables. In CSTNs, the controller cannot force the nature to choose a particular value for a propositional variable. However, he can put a lot of pressure on her to choose the value he wants. Indeed, we next describe a network (in the standard framework of CSTNs) that allows the controller to specify the value he desires for a variable x i , by executing one among two particular actions, one for true and one for false. The network is built in such a way that, if the value actually chosen by the nature differs from the prescription of the planner, then he is able to schedule the rest of the network easily, satisfying all the remaining constraints. Thanks to this property, the nature is effectively obliged to choose the variables as specified by the planner, otherwise she is doomed to lose the match.
We begin with an informal description of our construction Γ Φ . Figure 1 shows an example of our construction for n = 3, and may help the reader in following the exposition. There are n gadgets G 1 , . . . , G n connected in series. The i-th gadget G i involves the propositional variables x i , y i (which are now normal variables chosen by the nature), and two extra variables c 1 i and c 0 i . The purpose of G i is to let the controller choose the value of x i , and then observe the value of y i chosen by the nature. The nodes of Moreover, G i connects also to the nodes A i+1 and B i+1 which, for i < n, belong to the next gadget G i+1 , while A n+1 and B n+1 are two extra nodes at the end of the construction. It is here, between A n+1 and B n+1 , that the m clause constraints get lied down. For each j = 1, . . . , m, we put a constraint B n+1 − A n+1 ≥ n + 1 with label j := ¬l j,1 ∧ ¬l j,2 ∧ ¬l j,3 , defined as the negation of the j-th clause of ϕ, like in the toy reduction of the previous section.
Before describing the internals of each gadget, we show how they play together and we focus only on the tasks A i and B i for i = 1, . . . , n + 1. Consider the constraint For the first gadget G 1 , the activation constraint B 1 − A 1 ≤ 0 is explicitly added to the network, without labels, enforcing the gadget G 1 to be always activated. Thanks to the internal structure of the gadgets, the activation constraint is then propagated from one gadget to the next, as long as the nature chooses the value of x i according to the prescription of the controller. If the nature always chooses x i according to the controller, then all the gadgets are activated and we end up with the propagated constraint B n+1 − A n+1 ≤ n. At this point, the controller is able to schedule A n+1 and B n+1 if and only if all the clauses of ϕ are satisfied, so that the constraints B n+1 − A n+1 ≥ n + 1 labeled with i are all void.
If instead the nature chooses for any x i the opposite value to the one prescribed, then the activation constraint on A i and B i is not propagated to A i+1 and B i+1 , the following gadgets are not activated, and the controller is able to execute all the other tasks B i , C h i and D i for i > i very far in the future, without violating any constraint.
We now describe the internal mechanism of each gadget. At the heart of G i there are the two constraints D i ≤ B i + 1 and D i ≥ A i + (n + 2), labeled with c 1 i ∧ c 0 i and ¬c 1 i ∧ ¬c 0 i respectively. If the gadget is activated, then these two constraints cannot be satisfied together (since B i − A i ≤ i − 1 ≤ n). Hence, the controller has to observe either c 1 i or c 0 i , in order to decide whether to execute D i early or not (see Lemma 3). Which of the two variables is observed specifies the desired value of x i : so, if the planner wants x i to be true, then he should execute C 1 i , and if he wants x i to be . . Figure 1. Reduction from Q3SAT to CSTN-DC for n = 3. A Q3SAT formula Φ = ∃x 1 ∀y 1 ∃x 2 ∀y 2 ∃x 3 ∀y 3 m j=1 (l j,1 ∨ l j,2 ∨ l j,3 ) is transformed into the network Γ Φ illustrated above, where nodes denote tasks and edges denote constraints. Specifically, a directed edge labeled δ, from a node N to a node M denotes the labeled constraint (M ≤ N + δ, ). The label j is defined as the negation of the j-th clause of the 3CNF formula, i.e., j := ¬l j,1 ∧ ¬l j,2 ∧ ¬l j,3 . The empty label λ is omitted. A label q? beside a node Q indicates that Q = O(q).
false, he should execute C 0 i . A constraint X i ≥ A i + (n + 2) ensures that the controller can observe x i only after choosing either C 1 i or C 0 i . Then, the constraint Y i ≥ X i + 1 allows the controller to observe y i only after x i , and the constraint A i+1 ≥ Y i + 1 connects to the next gadget.
The propagation of the activation constraint B i − A i ≤ i − 1 to the next gadget is achieved by the two constraints B i+1 ≤ C 1 i + (n + 4) and B i+1 ≤ C 0 i + (n + 4), labeled with x i and ¬x i respectively. In order for the propagation to take place, the nature has to choose x i to true if C 1 i has been executed, and to false if C 0 i has been executed (see Lemma 5).
The full construction is provided for reference in Figure 2, and it is illustrated in Figure 1 for n = 3. The execution strategy σ is defined in Figure 3, where b (s) := min{b(s), n} and ∞ denotes a sufficiently large value, say, ∞ := (n + 4)(n + 2).
..,n, L(N ) = λ for every N ∈ T , C contains the following constraints: (B1 − A1 ≤ 0, λ), for i = 1, . . . , n:  Notice that the value [σ(s)] N for a task N ∈ T and a scenario s depends on the value s(p) only for those variables p ∈ P that are observed strictly before the time point [σ(s)] N . This condition is sufficient to guarantee that σ is dynamic. In particular, observe that the condition i ≤ b(s) depends only on the variables x 1 , y 1 , . . . , x i−1 , y i−1 , and that [σ(s)] Di for i ≤ b (s) depends on either c 0 i or c 1 i , whichever has been actually observed at time (n + 4)i in the scenario s.
One can easily check that σ is viable, by checking that all the constraints in C are satisfied. In particular, concerning the constraints (B n+1 ≥ A n+1 + (n + 1), ¬l j,1 ∧ ¬l j,2 ∧ ¬l j,3 ) for j ∈ {1, . . . , m}, there are two possibilities. If b(s) =  To prove the converse of Lemma 2, we first spot out three facts detailing out how the gadgets work as intended. First, if the i-the gadget is activated, then the controller is forced to execute either C 0 i or C 1 i early (Lemma 3). Second, the activation of the i-th gadget and the choice of either C 0 i or C 1 i cannot depend on the variables x i , y i , . . . , x n , y n , so the nature can choose their values "later on" (Lemma 4). Third, if the nature copies the value selected by the controller, the activation constraint is propagated to the next gadget (Lemma 5).
, then the constraint D i ≤ B i + 1 applies in scenario s and is violated by σ(s ). Otherwise, if d = 0, the constraint D i ≥ A i + n + 1 applies in scenario s and is violated by σ(s ). In either case, this contradicts the fact that σ is viable.
Lemma 4 (The nature can choose future variables). Let σ be a viable and dynamic execution for Γ Φ . Let s be any scenario and i ∈ {1, . . . , n}. Let s = s[v/p] be a scenario obtained by changing the value of any variable p ∈ {x i , y i , . . . , x n , y n } to any value v ∈ {0, 1}. Then, we have Proof: Let f : {0, 1} * → {0, 1} be the winning strategy of the universal player for Φ. Suppose by contradiction that σ is a viable and dynamic execution strategy for Γ Φ .
We first construct, for I = 0, . . . , n, step by step, a scenario s I such that Consider the scenario s n . We have (a) [σ(s n )] Bn+1 − [σ(s n )] An+1 ≤ n. Moreover, by (b) and the fact that f is a winning strategy for the universal player, the formula ϕ is false in the interpretation given by the scenario s n . In particular, some clause is not satisfied, say, the j-th clause for some j ∈ {1, . . . m}. So, the constraint B n+1 − A n+1 ≥ n+1 labeled with j applies in scenario s n , but it is violated since we proved [σ(s n )] Bn+1 − [σ(s n )] An+1 ≤ n.
Proof: Given a Q3SAT formula Φ, the CSTN Γ Φ can be easily constructed within logarithmic internal memory. By Lemmas 2 and 6, it is dynamically controllable iff Φ ≡ true.

A. Relative execution strategies
First, we extend some of the notions for CSTNs to the case when some of the tasks have already been performed. This will be crucial to describe our inductive polynomialspace algorithm.
Definition 15 (Partial schedule, next action, completion). A partial schedule over T up to time t ∈ R is a schedule ψ over a subset Dom(ψ) ⊆ T , such that [ψ] X ≤ t for every X ∈ Dom(ψ). Given a partial schedule ψ up to time t, a next action for ψ is a pair (t next , T next ) where t next > t is a time point and T next ⊆ T \ Dom(ψ) is a non-empty set of temporal variables not assigned by ψ. Let ψ[t next /T next ] = ψ ∪ {(X, t next ) | X ∈ T next } be the partial schedule, up to time t next , obtained from ψ by further executing all the actions in T next at time t next . Given a partial schedule ψ up to time t, a completion of ψ is a schedule ψ ∈ Ψ T such that [ψ ] X = [ψ] X for every X ∈ Dom(ψ) and [ψ ] X > t for every X ∈ Dom(ψ ) \ Dom(ψ). Let Ψ T [ψ] be the set of completions of ψ.
Definition 16 (Observation, completion of a partial scenario). Given a partial scenario h and a set of propositional variables P ⊆ P \ Dom(h) not assigned by h, an observation of P is a function o : P → {0, 1}, and h ∪ o is the partial scenario obtained from h by adding all the assignments given by o. Given a partial scenario h, a completion of h is a total scenario s ∈ Σ P such that s(p) = h(p) for every p ∈ Dom(h). Let Σ P [h] denote the set of completions of h.
Definition 19 (Relative execution strategies). A relative execution strategy from a configuration c = (t, ψ, h) is a function σ : Σ P [h] → Ψ T [ψ] that maps each scenario s which is a completion of h to a total schedule σ(s), over T s , which is a completion of ψ. A relative execution strategy σ is viable if σ(s) is feasible for Γ s for every scenario s ∈ Σ P [h]. It is dynamic if, for any scenarios s, s ∈ Σ P [h] and time variable X ∈ T s , letting t = [σ(s)] X , if Hist(t, s, σ) = Hist(t, s , σ) then X ∈ T s and [σ(s )] X = t. Observe that a (dynamic, viable) relative execution strategy from the initial configuration c 0 is a (dynamic, viable) execution strategy and vice-versa.
Definition 20 (Dynamic controllability from a configuration). A CSTN is dynamically controllable from a configuration c if it admits a dynamic and viable relative execution strategy from c.
The following definition and lemma serve to ensure that, in a dynamic relative execution strategy from a non-terminal configuration, there is always a set of actions that is executed next, all at the same time across all the scenarios.

Lemma 7.
If σ is a dynamic execution strategy from a non-terminal configuration c = (t, ψ, h), then σ has a welldefined next action.
Proof: Since σ is non-terminal there exist some s ∈ Σ P [h] and X ∈ T s \ Dom(ψ). Therefore, we can define t next (σ) = min s∈Σ P [h],X∈Ts\Dom(ψ) [σ(s)] X . Then, we choose any s 0 ∈ Σ P [h] and define T next (σ) = {X ∈ T s0 | [σ(s 0 )] X = t next (σ)}. We prove that T next (σ) does not depend on the choice of s 0 , using the fact that σ is dynamic, and this concludes the proof.
Definition 22 (Child configurations and strategies). Suppose σ has a well-defined next action. Let P next (σ) = {p ∈ P | O(p) ∈ T next (σ)} be the set of propositional variables observed at time t next (σ) and o : P next (σ) → {0, 1} be any outcome for the observations. Define the Proof: Since child (σ, o) is a restriction of σ, there are less pairs s, s ∈ Σ P that need to be checked in order for child (σ, o) to be dynamic.
Lemma 9. Let σ be a relative execution strategy from a non-terminal configuration c = (t, ψ, h). If σ has a welldefined next action and child (σ, o) is dynamic for every o : P next (σ) → {0, 1}, then σ is dynamic.
Proof: There exists only one execution strategy σ from c, defined by σ(s) = ψ for every s ∈ Σ P [h]. It is clearly dynamic, and, by definition, it is viable iff, for every scenario s ∈ Σ P [h], the schedule ψ is feasible for Γ s Lemma 12. A CSTN Γ is dynamically controllable from a non-terminal configuration c = (t, ψ, h) iff there exist a next action (T next , t next ) from ψ such that, for every observation o : P next → {0, 1} (where P next = {p ∈ P | O(p) ∈ T next }), Γ is dynamically controllable from c[t next /T next , o].
Proof: ( =⇒ ) Let σ be a dynamic and viable execution strategy from c. It is sufficient to apply Lemma 7 and take t next = t next (σ) and T next = T next (σ). Then, for every o : P next → {0, 1}, the strategy child (σ, o) is dynamic and viable from c[t next /T next , o], thanks to Lemma 8 and Lemma 10.
( ⇐= ) For every o : P next → {0, 1}, let σ o be a dynamic and viable execution strategy from c[t next /T next , o]. Then, define the strategy σ = o : Pnext →{0,1} σ o from the configuration c. Observe that σ has a well-defined next action, and in particular t next (σ) = t next and T next (σ) = T next . Moreover, for every o : P next → {0, 1}, we have child (σ, o) = σ o which is dynamic and viable by assumption. Thanks to Lemma 9 and Lemma 10, σ is dynamic and viable.
Lemma 11 (base case) and Lemma 12 (inductive case) suggest a recursive approach to solve CSTN-DC. In the inductive case, we need to consider all the possible choices of t next and T next . However, this is still not possible since t next is, a priori, an unbounded real number. In the following we show that, under suitable assumptions, we can choose t next among a finite set of possibilities.

B. Discrete strategies for CSTNs
We assume to work on CSTNs whose constraint bounds are discrete, and can be expressed with a finite number of bits in fixed-point precision. This is stated in the following definition.
Definition 23 (Discrete CSTN). Let w ∈ R and W ∈ N. A CSTN is (w, W )-discrete if, for every labeled constraint (Y ≤ X + δ, ) ∈ C, we have δ = kw for k ∈ {−W, . . . , +W }. We call Discrete CSTN-DC the variant of CSTN-DC where the input CSTN is (w, W )-discrete for some w ∈ R and W ∈ N.
We prove that, for discrete CSTNs, one can always restrict her attention to discrete execution strategies, whose execution times are expressible with a number of bits at most polynomial in the size of the input. Our proof is a generalization of an argument given in [5].
Then c s,Y ≤ c s,X , so also γ s,Y ≤ γ s,X and [σ (s)] Y − [σ (s)] X ≤ kw + (γ s,Y − γ s,X ) ≤ kw. (Dynamic.) The fact that an execution strategy is dynamic depends only on the relative order (in R) of the values of [σ(s)] X , which is preserved by our transformation to σ .

C. The algorithm
We first adapt Lemma 12 to relative execution strategies.
Proof: Trivial adaptation of the proof of Lemma 12. The polynomial-memory algorithm is a mere application of Lemma 13, Lemma 11 and Lemma 14. The pseudo-code is shown in Algorithm 1.
Proof: To implement the recursive procedure, it is sufficient to maintain a stack of triples (T 1 , k 1 , o 1 ) · · · (T l , k l , o l ) containing the choices of T next , k next and o at each level of the recursion. Indeed, the parameters ψ and h can be reconstructed from this stack. To represent the sequence k 1 , . . . , k l , we need O(|T | log |M |) = O(|T |(log |W | + log |T |)) bits, while T 1 , . . . , T l and o 1 , . . . , o l require only O(|T | log |T |) bits.
As a consequence we get the following.

D. Extending to real-valued CSTNs
It is possible to extend our polynomial algorithm so that it works without making any assumption on how the input numbers are encoded. Since Lemma 13 does not apply, we need a different way to limit the choice of t next to a finite set. We verified that it is sufficient to take t next among those linear combinations of the input numbers, having integer coefficients with a number of bits polynomial in the size of the network. A formal proof of this statement, as well as the extension of this positive result to CSTNUs, is subject of future work.

V. CONCLUSION
Our first result is a reduction from Q3SAT to CSTN-DC, which shows that checking the dynamic controllability of CSTNs is PSPACE-hard. Our reduction relies on the close interplay between labeled constrains and observation tasks, which allows the planner to effectively impose her choice on some of the propositional variables. This interplay seems to be the reason why CSTN-DC is difficult. On the other hand, the topology of the network plays very little role. Indeed, in our construction, the topology of the network is planar and extremely simple: there is only one directed cycle (observe that, if there was no directed cycle, then it would be trivially and strongly controllable), and removing a single edge, from A 1 to B 1 , we get an acyclic graph, and actually an inward arborescence (a directed rooted tree, where all edges point towards the root) when disregarding the parallel edges between A n and B n .
Our second result is an algorithm for CSTN-DC that uses only polynomial space, proving that CSTN-DC ∈ PSPACE.