The Expressive Power of Clocks

Thomas A. Henzinger, Peter W. Kopke, and Howard Wong-Toi

We investigate the expressive power of timing restrictions on labeled transition systems. In particular, we show how constraints on clock variables together with a uniform liveness condition--the divergence of time--can express Buchi, Muller, Streett, Rabin, and weak and strong fairness conditions on a given labeled transition system. We then consider the effect, on both timed and time-abstract expressiveness, of varying the following parameters: time domain (discrete or dense), number of clocks, number of states, and size of constants used in timing restrictions.

Proceedings of the 22nd International Colloquium on Automata, Languages, and Programming (ICALP), Lecture Notes in Computer Science 944, Springer, 1995, pp. 417-428.

Download inofficial, sometimes updated PostScript / PDF document. © 1995 Springer.