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.
Formal Methods in System Design, vol 24, pages 101-127 (FMSD 2004).
Journal version of [FS01].