## 4 Incremental Computation: Approach
 \tag{18}\]  
That is, \(next(t,t^{\prime})\) is defined only if \(t^{\prime}\) belongs to the part of timeline being considered. The above program is processed by Algorithm _Incremental_ (Algorithm 2). A graphical depiction of the steps of the algorithm is also provided in Figure 1.  
The algorithm leverages a fix-point computation to calculate a trajectory in an incremental fashion. The intuition is as follows. The algorithm takes as input a set of pre-determined time steps, e.g., corresponding to time steps that a user or external application would like to query about or about which observations are provided. Step 2 produces the grounding, \(G\), of _base_, \(p\), \(O\), and \(timedep(0)\). Due to the fact that \(p\) defines the pre-determined time steps, ground instances of the rules of \(timedep(0)\), which are time-dependent, are generated. Ground instances of external \(enabled(T)\) are also generated for every time step defined by \(p\). Let us recall that externals are false by default: step 3 changes this by asserting all externals from \(G\) true via the corresponding clingo primitive. At step 4, the answer set \(A\) of \(G\) is computed. If \(A\) does not contain any request for new time steps, then \(A\) encodes the trajectory that _Incremental_ aims at computing. Thus, all that is left is to ground \(output\) incrementally (step 16) and return the answer set of the updated grounding (step 17). ```
0:\(p\): pre-determined time steps, e.g., from observations and queries, as facts of the form \(time(t)\)
0:\(O\): a set of observations
0: an answer set
1:\(\triangleright\) Expansion phase (\(base+timedep(0)+p+O\))
2:\(G\gets ground(base\cuptimedep(0)\cup p\cup O)\)
3: For every external \(enabled(t)\) from G, assert \(enabled(t)\) true via clingo's \(assign\_external()\)
4:\(A\gets solve(G)\)
5:\(\triangleright\) end of expansion phase
6:while\(\{t\,|\,\mathit{newtime}(t^{\prime},t)\in A\text{ and }time(t)\
ot\in A\}\
eq\emptyset\)do
7:\(m\gets min\{t\,|\,\mathit{newtime}(t^{\prime},t)\in A\text{ and }time(t)\
ot\in A\}\)
8:\(\triangleright\) Expansion phase
9:\(G\gets ground(\{time(m).\})\)\(\triangleright\) add a new time step to the ground program
10:\(G\gets ground(timedep(m))\)
11: Assert \(enabled(m)\) true using clingo's \(assign\_external()\)
12:\(A\gets solve(G)\)
13:\(\triangleright\) end of expansion phase
14:endwhile
15:\(\triangleright\) addition of the output module
16:\(G\gets ground(output)\)
17:return\(solve(G)\)
```  
**Algorithm 2** Algorithm _Incremental_  
On the other hand, if the answer set computed at step 4 contains requests for new times steps, then those requests need to be satisfied. Let us recall that the introduction of a new time step may affect the calculation of the state of the domain at the time steps that follow it. For this reason, the algorithm first finds the minimum requested time step, \(m\) (step 7). Next, step 9 adds the requested time step to \(G\). Step 10 adds to \(G\) the groundings of all rules that compute the state of the domain at time steps \(m\) and later. Step 11 asserts \(enabled(m)\)  
Figure 1: Graphical depiction of the steps of _Incremental_. and step 12 calculates the updated answer set \(A\) of \(G\). At this point, the algorithm verifies whether \(A\) contains any requests for new time steps and the process repeats. Let us now focus on the soundness and completeness of Algorithm _Incremental_ with regard to the corresponding non-incremental way of computing the trajectory. To begin, we define the _single-shot version_ of the program \(\Pi\) used by _Incremental_, which is obtained from \(\Pi\) by (a) removing all \(\#program\) declarations, and (b) adding to each program the following rules:  
\[ \begin{array}{l}\#const\ t=0.\\ time(T)\gets newtime(T^{\prime},T).\\ enabled(T)\gets time(T).\end{array}  \tag{19}\]  
The first statement assigns value \(0\) to constant \(t\), thereby making all conditions of the form \(T\geq t\) (from the pair of conditions \(enabled(T)\), \(T\geq t\)) trivially satisfied.