An implementation of three algorithms for timing verification based on automata emptiness

Three algorithms for checking the emptiness of a timed transition system have been implemented. The first algorithm performs a straightforward reachability analysis on sets of states of the system, rather than on individual states. This corresponds to stepping symbolically through the system many states at a time. The other two algorithms are minimization algorithms. These simultaneously perform reachability analysis and minimization from an implicit system description. The paradigm for verification is to test for the emptiness of the set of all timed system executions that violate a requirements specification. Preliminary results over two simple examples indicate that memory usage is a more limiting factor than time