|
Abstract : |
Abstract. We explain here how the bottom-up evaluation method of Revesz for recursive programs with arithmetic constraints, can be adapted from the domain of integers to the domain of reals. We apply the procedure to characterize the set of ancestors of a given state H for timed automata. (An ancestor of H is a state linked to H by a sequence of transitions.) Such a procedure also applies to extensions of timed automata where, in particular, real variables are used not only as clocks but as data registers. The procedure has been successfully experimented for proving automatically the correctness of a sophisticated reactive program that controls dataflow rates on ATM networks. 1, |
