--- _id: '4607' abstract: - lang: eng text: We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem. acknowledgement: "A preliminary version of this paper appeared in the Proceedings of the Fifth International Conference on Computer-Aided Verification (CAV 93), Springer-Verlag LNCS 818, pp. 181–193, 1993. We thank Sergio Yovine for a careful reading of the manuscript. This reaserch was partially supported by the BRA ESPRIT project REACT, by the ONR YIP\r\naward N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grants CCR-9200794 and CCR-9504469, by the AFOSR contract F49620-93-1-0056, and by the ARPA grant NAG2-892." article_processing_charge: No article_type: original author: - first_name: Rajeev full_name: Alur, Rajeev last_name: Alur - first_name: Costas full_name: Courcoubetis, Costas last_name: Courcoubetis - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 citation: ama: Alur R, Courcoubetis C, Henzinger TA. Computing accumulated delays in real-time systems. Formal Methods in System Design. 1997;11(2):137-156. doi:10.1023/A:1008626013578 apa: Alur, R., Courcoubetis, C., & Henzinger, T. A. (1997). Computing accumulated delays in real-time systems. Formal Methods in System Design. Springer. https://doi.org/10.1023/A:1008626013578 chicago: Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “Computing Accumulated Delays in Real-Time Systems.” Formal Methods in System Design. Springer, 1997. https://doi.org/10.1023/A:1008626013578. ieee: R. Alur, C. Courcoubetis, and T. A. Henzinger, “Computing accumulated delays in real-time systems,” Formal Methods in System Design, vol. 11, no. 2. Springer, pp. 137–156, 1997. ista: Alur R, Courcoubetis C, Henzinger TA. 1997. Computing accumulated delays in real-time systems. Formal Methods in System Design. 11(2), 137–156. mla: Alur, Rajeev, et al. “Computing Accumulated Delays in Real-Time Systems.” Formal Methods in System Design, vol. 11, no. 2, Springer, 1997, pp. 137–56, doi:10.1023/A:1008626013578. short: R. Alur, C. Courcoubetis, T.A. Henzinger, Formal Methods in System Design 11 (1997) 137–156. date_created: 2018-12-11T12:09:43Z date_published: 1997-01-01T00:00:00Z date_updated: 2022-08-16T13:43:41Z day: '01' doi: 10.1023/A:1008626013578 extern: '1' intvolume: ' 11' issue: '2' language: - iso: eng month: '01' oa_version: None page: 137 - 156 publication: Formal Methods in System Design publication_identifier: issn: - 0925-9856 publication_status: published publisher: Springer publist_id: '98' quality_controlled: '1' scopus_import: '1' status: public title: Computing accumulated delays in real-time systems type: journal_article user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 11 year: '1997' ...