The benefits of relaxing punctuality

R. Alur, T. Feder, T.A. Henzinger, Journal of the ACM 43 (1996) 116–146.

Download
No fulltext has been uploaded. References only!

Journal Article | Published
Author
; ;
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
Volume
43
Issue
1
Page
116 - 146
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, 43(1), 116–146. 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 43, no. 1 (1996): 116–46. 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, 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.

Link(s) to Main File(s)
Access Level
Restricted Closed Access

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar