Automata generation for on-the-fly automatic verification using formulas of an interval logic

This paper looks at the application of Future Interval Logic (FIL) to the automatic verification of temporal logic interval formulas. An algorithm is developed to construct a Buchi automaton which is semantically equivalent to a system specification described by means of FIL formulas. The algorithm is intended to be used within the framework of on-the-fly model checking methods as a way of solving the problem of verifying reactive systems. A set of expansion rules is obtained from a formally defined reduction relation and from the FIL semantics. The algorithm uses these rules to reduce a formula into simpler ones, which are satisfied by the states of the automaton run. The acceptance conditions are determined by a new procedure. Finally, some experimental results obtained with it are presented