The benefits of relaxing punctuality Journal Article

Author(s): Alur, Rajeev; Feder, Tomás; Henzinger, Thomas A
Article Title: The benefits of relaxing punctuality
Abstract: The most natural, compositional, way of modeling real-time systems uses a dense domain for time. The satisfiability 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.
Journal Title: Journal of the ACM
Volume: 43
Issue 1
ISSN: 0004-5411
Publisher: ACM  
Date Published: 1996-01-01
Start Page: 116
End Page: 146
DOI: 10.1145/227595.227602
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work