The benefits of relaxing punctuality
Alur R, Feder T, Henzinger TA. 1996. The benefits of relaxing punctuality. Journal of the ACM. 43(1), 116–146.
Download
No fulltext has been uploaded. References only!
Journal Article
| Published
| English
Scopus indexed
Author
Alur, Rajeev;
Feder, Tomás;
Henzinger, Thomas AISTA 
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.
Publishing Year
Date Published
1996-01-01
Journal Title
Journal of the ACM
Acknowledgement
We wish to thank an anonymous referee for pointing out the PSPACE-fragment of Section 4.5.
Volume
43
Issue
1
Page
116 - 146
ISSN
IST-REx-ID
Cite this
Alur R, Feder T, Henzinger TA. The benefits of relaxing punctuality. Journal of the ACM. 1996;43(1):116-146. doi:10.1145/227595.227602
Alur, R., Feder, T., & Henzinger, T. A. (1996). The benefits of relaxing punctuality. Journal of the ACM. ACM. https://doi.org/10.1145/227595.227602
Alur, Rajeev, Tomás Feder, and Thomas A Henzinger. “The Benefits of Relaxing Punctuality.” Journal of the ACM. ACM, 1996. https://doi.org/10.1145/227595.227602.
R. Alur, T. Feder, and T. A. Henzinger, “The benefits of relaxing punctuality,” Journal of the ACM, vol. 43, no. 1. ACM, pp. 116–146, 1996.
Alur R, Feder T, Henzinger TA. 1996. The benefits of relaxing punctuality. Journal of the ACM. 43(1), 116–146.
Alur, Rajeev, et al. “The Benefits of Relaxing Punctuality.” Journal of the ACM, vol. 43, no. 1, ACM, 1996, pp. 116–46, doi:10.1145/227595.227602.
Google Scholar