The benefits of relaxing punctuality

The most natural, compositional, way of modeling real-time systems uses a dense domain for time. The satistiability 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. Categories and Subject Descriptors: C.3 (Special-Purpose and Application-Based Systems)--real- time systems; D.2.1 (Software Engineeriogk Requirements/Specifications-languages; F.3.1 (Lugics and Meanings of ~rugmms): Specifying and Verifying and Reasoning about Programs-lo& of programs; mechanical verification; specification techniques; F.4.3 (Mathematical Logic and Formal Languages): Formal Languages-classes f decision problems