This paper is broadly concerned with formal verification of timed systems. A well-known model of timed systems is the timed automaton, which is a class of finite state machine (FSM), equipped with one or more clocks for measuring the lapse of time. Verification of timed systems using timed automata is an intense research area that has led to efficient methods and tools. One common idea for verification is to convert timed automata into standard FSMs that can then be analyzed using traditional verification techniques. Region automata and zone-closed simulation graphs are some of the classes of FSMs used for this purpose; region automata were the earliest to establish the solvability of the verification problem, while zone-closed simulation graphs are more efficient versions used in verification tools for timed systems. The soundness of these tools hinges on the fact that zone graphs are correct for checking emptiness of timed automata--this fact was recently established.

Timed automata are useful for the verification of safety properties of timed systems. A standard extension called timed Büchi automata (TBA) is proposed for expressing and verifying liveness properties of timed systems. The idea of region automata and zone-graph construction is useful for verifying TBA. While reachability computation is at the core of verification of safety properties, detecting cycles in the region automata and zone graph is the technique used for verification of TBA. An important question in this regard is, once again, the question of correctness: does the presence of cycles in the zone graph imply the presence of cycles in the TBA?

The primary goal of this paper is to answer this question positively, to justify the use of zone graphs in the methods and tools for verification of liveness properties of timed systems. Specifically, the paper shows that for the class of diagonal-free TBA, constructing a zone-graph approximation of the automata and determining the existence of cycle in the latter determine the verification of TBA. This result is obtained from a similar result established for region-closed graphs, using the construction for establishing the result for plain reachability.

The paper is technical and accessible to specialists who are already working in the area. It is very well written and gives a lot of intuitive results, with moderate illustration. The paper contains a good summary of many important results, with pointers to related works in the area. I definitely recommend it to people who are interested in understanding the theoretical underpinnings of verification of timed systems, based on timed automata.