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