--- _id: '4620' abstract: - lang: eng text: We present a verification algorithm for duration properties of finite-state real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated time during which certain state predicates hold. We formalize the concept of durations by introducing duration measures for (dense-time) timed automata. Given a timed automaton with a duration measure, a start and a target state, and a duration constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the start state to the target state such that the accumulated duration along the run satisfies the constraint. Our main result is a novel decision procedure for solving the duration-bounded reachability problem. We also prove that the problem is PSPACE-complete and demonstrate how the solution can be used to verify interesting duration properties of real-time systems. acknowledgement: BRA ESPRIT project REACT, National Science Foundation grant CCR-9200794 United States Air Force Office of Scientific Research contract F49620-93-1-0056 alternative_title: - LNCS article_processing_charge: No 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. In: 5th International Conference on Computer Aided Verification. Vol 697. Springer; 1993:181-193. doi:10.1007/3-540-56922-7_16' apa: 'Alur, R., Courcoubetis, C., & Henzinger, T. A. (1993). Computing accumulated delays in real-time systems. In 5th International Conference on Computer Aided Verification (Vol. 697, pp. 181–193). Elounda, Greece: Springer. https://doi.org/10.1007/3-540-56922-7_16' chicago: Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “Computing Accumulated Delays in Real-Time Systems.” In 5th International Conference on Computer Aided Verification, 697:181–93. Springer, 1993. https://doi.org/10.1007/3-540-56922-7_16. ieee: R. Alur, C. Courcoubetis, and T. A. Henzinger, “Computing accumulated delays in real-time systems,” in 5th International Conference on Computer Aided Verification, Elounda, Greece, 1993, vol. 697, pp. 181–193. ista: 'Alur R, Courcoubetis C, Henzinger TA. 1993. Computing accumulated delays in real-time systems. 5th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 697, 181–193.' mla: Alur, Rajeev, et al. “Computing Accumulated Delays in Real-Time Systems.” 5th International Conference on Computer Aided Verification, vol. 697, Springer, 1993, pp. 181–93, doi:10.1007/3-540-56922-7_16. short: R. Alur, C. Courcoubetis, T.A. Henzinger, in:, 5th International Conference on Computer Aided Verification, Springer, 1993, pp. 181–193. conference: end_date: 1993-07-01 location: Elounda, Greece name: 'CAV: Computer Aided Verification' start_date: 1993-06-28 date_created: 2018-12-11T12:09:47Z date_published: 1993-01-01T00:00:00Z date_updated: 2022-03-21T13:55:53Z day: '01' doi: 10.1007/3-540-56922-7_16 extern: '1' intvolume: ' 697' language: - iso: eng main_file_link: - url: https://link.springer.com/chapter/10.1007/3-540-56922-7_16 month: '01' oa_version: None page: 181 - 193 publication: 5th International Conference on Computer Aided Verification publication_status: published publisher: Springer publist_id: '89' quality_controlled: '1' scopus_import: '1' status: public title: Computing accumulated delays in real-time systems type: conference user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17 volume: 697 year: '1993' ...