Fast detection of cycles in timed automata
Abstract: We will present an algorithm to detect if a cycle in a timed automaton can be iterated infinitely often. Existing solutions in tools have a complexity which is exponential in the number of clocks. Our method is polynomial. This method can be incorporated in algorithms for verifying Büchi properties on timed automata. Experiments show a significant reduction in search space.
This is joint work with A. Deshpande, F. Herbreteau, T.T. Tran and I.