Grigore, Distefano, Petersen, Tzevelekos,
Runtime Verification Based on Register Automata, TACAS2013
Operations:
 ${\it add\_child}$ (click)
 ${\it deactivate}$ (ctrlclick)
 collect (button)
Legend:
 active
 needed
 unneeded
 numbers are distances to
active
descendant
 ‘needed’ = ‘labeled by $\lt h$’
($h=4$ in this example)
Operations:
 ${\it add\_child}$ (click)
 ${\it deactivate}$ (ctrlclick)
Legend:
 active
 needed
 unneeded
 scheduled for deletion
 numbers are distances from root
Theorem
Consider a sequence of $\ell$ updates for the realtime tree buffer.

Every update takes constant time.

${}^{(k)}\in O(\max_{j\le k}$
${}^{(j)})$
for all $k \le \ell$.

${}^{(k)}\in O($
${}^{(k)})$
for all $k \le \ell$,
if the sequence is extensive.
Example Applications
 runtime verification: error traces
 regex searching: capturing groups
 tracing infinite automata with relevant/irrelevant transitions