Real-time systems play an increasingly important role in applications ranging from telecommunication systems to computer controlled physical systems. An important model for specifying and analyzing real-time systems is the timed automata model. A timed automaton is an automaton coupled with a finite number of continuous clocks. In this talk, I will discuss the verification problem for timed automata. The simplest verification problem is the reachability problem --- whether some undesirable states of the system are reachable from the initial state.

I will show that the standard method for solving the reachability problem for timed automata is not ``correct''. I will then present a new formulation of the reachability problem for timed automata. I will present an algorithm to solve the new problem and provide an outline for its proof of correctness. I will illustrate the timed automata verification problem with a simple robot-controller example.