# Querying and Extracting Timeline Information from Road Traffic Sensor Data
## 5 Timeline Query Index and Analytical Query Processing
### TQ-index Construction
#### Congestion Event Detection
In this example, \(L_{1}\) has three and \(L_{2}\) has two congestion events._

The correctness of the aggregation query processing algorithm is proven by following a loop-invariant verification technique. Figure 15: Aggregation query example. **Theorem 5**: **. ** _[Correctness of aggregation query processing] The aggregation query processing algorithm is correct with two given loop invariants: In the first loop, \(H\) is empty or contains a critical key; for the second loop invariant, the number of \(A\) is the same as the number of iterations._

**Proof. ** Before the iteration begins, assume that \(TM\) is the result of basic query processing, \(C\) is a finite set of traffic congestion from \(TM\), and \(H\) is an empty hash map. **Initialization:** (First Loop) At the beginning, \(H\) is empty, trivially. **Maintenance:** (First Loop) For any steps in the iteration, if \(H\) does not contain a value of \(key\) as keys, then a new list will be inserted to \(H\) with the value of \(key\) as a key. **Termination:** (First Loop) After the last iteration, we guarantee that \(H\) contains a value \(key\) as a key, which is explained in the maintenance part. **Initialization:** (Second Loop) At the beginning of the loop, a step number \(i\) is initialized to \(0\), and \(A\) is still empty. **Maintenance:** (Second Loop) For each iteration, the new value from AGGREGATION-FUNCTION will be included as an element of \(A\). Thus, at the \(i\)th iteration step, when \(i>0\), the number of \(A\) equals \(i\). When we move to the next iteration step \(i+1\)th, a new value for the group \(gr\) will be added to \(A\) again, which leads to an increase in the number of elements \(A\) to \(i+1\). **Termination:** (Second Loop) At the end of the iteration, the value \(i\) is equal to the size of \(H\), and the number of elements in \(A\) would be the same as \(H\). Thus, the number of elements in \(A\) would be exactly the same as \(i\). **Correctness:** Both loop invariant methods are working with the finite sets. Thus, they are always terminated and produce the correct results. #### 5.3.3. Affected Congestion Query Processing

An affected congestion query \(Q_{4}\) requires the exploitation of the affectedness list, which is built during the CalculateDependency algorithm. For the affected congestion, we proceed with the results of the timeline model, as shown in Figure 14.

Algorithm 8 explains the procedures. First, we invoke BasicQueryProcessing to obtain a timeline model. After obtaining a set of congestion events, we simply track the \(affecting\) pointers for each congestion's node until we reach the last (lines 5 to 7). ```
Input: A TQ-index \(tqi\), a set of LinkIDs \(L\), a start Time \(t_{start}\), an end time \(t_{end}\) Output: A set of congestions \(ret\)
1:procedureAffectedCongStoVeryProcessing(\(tqi\), \(t_{start}\), \(t_{end}\), \(lid\))
2:A timeline model \(TM\leftarrow\)BasicQueryProcessing(\(tqi\), \(L\), \(t_{start}\), \(t_{end}\));
3:\(C\leftarrow\)GetCongSto(\(TM\));
4:A set of affected congestions \(RET\leftarrow\)NULL;
5:foreach congestion \(c\) in \(C\)do
6:if\(c.affecting\) is not NULLthen\(RET\)Add(\(.affecting\));
7:endforeach
8:returnRET;
```

**Algorithm 8**Affected Congestions Query Processing

The correctness of the affected congestions query processing algorithm is proved by following a loop invariant verification technique. **Theorem 6**: **. ** _[Correctness of affected congestion query processing] The affected congestion query processing algorithm is correct with a given loop invariant: At the start of the loop, the number of elements in RET is equal to or greater than the number of iteration steps._

**Proof. ** **Initialization:** (Second Loop) At the beginning of the loop, a step number \(i\) is initialized to 0 and \(RET\) is still empty. **Maintenance:** For each iteration, the newly affected congestion from congestion \(c\) will be included as an element of \(RET\). Thus, at the \(i\)th iteration step, when \(i>0\), the number of \(RET\) equals \(i\).