THE BENEFITS OF RELAXING PUNCTUALITY

The most natural, compositional, way of modeling real-time systems use s a dense domain for time. The satisfiability of timing constraints th at are capable of expressing punctuality in this model however, is kno wn to be undecidable. We introduce a temporal language that can constr ain 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 timi ng properties of real-time systems with a dense semantics.