Checking Finite Traces using Alternating Automata

Bernd Finkbeiner and Henny Sipma

We present three algorithms to check at runtime whether a reactive program satisfies a temporal specification, expressed by a future linear-time logic formula. The three methods are all based on alternating automata, but traverse the automaton in different ways: depth-first, breadth-first, and backwards, respectively. All three methods have been implemented and experimental results are presented. We outline an extension to these algorithms that is applicable to LTL formulas containing both past and future operators.

Runtime Verification 2001 (RV’01). Electronic Notes in Theoretical Computer Science, Volume 55, Number 2, link (RV 2001).

(pdf) (bib)