Computing accumulated delays in real-time systems

R. Alur, C. Courcoubetis, T.A. Henzinger, in:, Springer, 1993, pp. 181–193.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published
Author
; ;
Series Title
LNCS
Abstract
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.
Publishing Year
Date Published
1993-01-01
Acknowledgement
BRA ESPRIT project REACT, National Science Foundation grant CCR-9200794 United States Air Force Office of Scientific Research contract F49620-93-1-0056
Volume
697
Page
181 - 193
Conference
CAV: Computer Aided Verification
IST-REx-ID

Cite this

Alur R, Courcoubetis C, Henzinger TA. Computing accumulated delays in real-time systems. In: Vol 697. Springer; 1993:181-193. doi:10.1007/3-540-56922-7_16
Alur, R., Courcoubetis, C., & Henzinger, T. A. (1993). Computing accumulated delays in real-time systems (Vol. 697, pp. 181–193). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/3-540-56922-7_16
Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “Computing Accumulated Delays in Real-Time Systems,” 697:181–93. Springer, 1993. https://doi.org/10.1007/3-540-56922-7_16.
R. Alur, C. Courcoubetis, and T. A. Henzinger, “Computing accumulated delays in real-time systems,” presented at the CAV: Computer Aided Verification, 1993, vol. 697, pp. 181–193.
Alur R, Courcoubetis C, Henzinger TA. 1993. Computing accumulated delays in real-time systems. CAV: Computer Aided Verification, LNCS, vol. 697. 181–193.
Alur, Rajeev, et al. Computing Accumulated Delays in Real-Time Systems. Vol. 697, Springer, 1993, pp. 181–93, doi:10.1007/3-540-56922-7_16.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar