Alur, Rajeev ; Feder, Tomás ; Henzinger, Thomas AIST Austria
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 of the ACM
116 - 146
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)