Report Number: CS-TR-91-1359
Institution: Stanford University, Department of Computer Science
Title: The benefits of relaxing punctuality
Author: Alur, Rajeev
Author: Feder, Tomas
Author: Henzinger, Thomas A.
Date: May 1991
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.