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.