BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-91-1359
       ENTRY:: September 01, 1994
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: The benefits of relaxing punctuality
        TYPE:: Technical Report
      AUTHOR:: Alur, Rajeev
      AUTHOR:: Feder, Tomas
      AUTHOR:: Henzinger, Thomas A.
        DATE:: May 1991
       PAGES:: 40
    ABSTRACT:: The most natural, compositional way of modeling real-time
               systems uses a dense domain for time. The satisfiability of
               real-time constraints that are capable of expressing punctuality
               in this model is, however, 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.
       NOTES:: [Adminitrivia V1/RAM/19940901]
         END:: STAN//CS-TR-91-1359