---
_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'
...