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 February 2004
Contact Data Privacy Policy Imprint
Home People Publications
More