Benefits of Relaxing Punctuality

摘要

The most natural, compositional way of modeling real-time systems uses a densedomain for time. The satisfiability of real-time constraints that are capable of expressing punctuality in this model is, however, known to be undecidable. The authors 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 EXPACE-complete. This result allows the authors to develop an algorithm for the verification of timing properties of real-time systems with a dense semantics.