## The Benefits of Relaxing Punctuality

*Rajeev Alur, Tomas Feder, and
Thomas A. Henzinger*
The most natural, compositional, way of modeling real-time systems uses a
dense domain for time.
The satisfiability of timing constraints that are capable of expressing
punctuality in this model, however, is known to be undecidable.
We introduce a temporal language that can constrain the time difference
between events only with finite, yet arbitrary, precision and show the
resulting logic to be EXPSPACE-complete.
This result allows us to develop an algorithm for the verification of timing
properties of real-time systems with a dense semantics.

*Journal of the ACM* 43:116-146, 1996.
A preliminary version appeared in the
*Proceedings of the
Tenth Annual ACM Symposium on Principles of Distributed Computing*
(PODC 1991), pp. 139-152.