Checking Finite Traces using Alternating Automata

Bernd Finkbeiner, Henny Sipma

We present three algorithms to check at runtime whether a reactive program satisfies a temporal specification, expressed by a future linear-time temporal 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.

In Runtime Verification, CAV'01 workshop.

Postscript, PDF.


© Henny Sipma / sipma@cs.stanford.edu
Last modified: Tue Jul 17 15:29:42 PDT 2001