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 Symposium on Principles of Distributed Computing (PODC), ACM Press, 1991, pp. 139-152.