Tree Buffers

Radu Grigore and Stefan Kiefer

University of Oxford

CAV 2015, San Francisco

a b a b,c a,c b a,b,c

Grigore, Distefano, Petersen, Tzevelekos, Runtime Verification Based on Register Automata, TACAS2013

Linear Buffer

Circular Buffer

Tree Buffer

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)

Real-Time Tree Buffer

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

http://arxiv.org/abs/1504.04757