### Anuj Puri

### Bell Labs

### Verification of Real-time Systems

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.