Grigore, Distefano, Petersen, Tzevelekos,
Runtime Verification Based on Register Automata, TACAS2013
Operations:
- ${\it add\_child}$ (click)
- ${\it deactivate}$ (ctrl-click)
- 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}$ (ctrl-click)
Legend:
- active
- needed
- unneeded
- scheduled for deletion
- numbers are distances from root
Theorem
Consider a sequence of $\ell$ updates for the real-time 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