Abstract
We consider the timed automata model of [3], which allows the analysis of real-time systems expressed in terms of quantitative timing constraints. Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, we may wish to express the likelihood of the system making certain transitions. In this paper, we present a model for real-time systems augmented with discrete probability distributions. Furthermore, using the algorithm of [5] with fairness, we develop a model checking method for such models against temporal logic properties which can refer both to timing properties and probabilities, such as, “with probability 0.6 or greater, the clock x remains below 5 until clock y exceeds 2”
supported in part by EPSRC grant GR/M04617
supported in part by EPSRC grant GR/M13046
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
R. Alur, C. Courcoubetis, and D. Dill. Model-checking for probabilistic real-time systems. In Automata, Languages and Programming: Proceedings of the 18th ICALP, Lecture Notes in Computer Science 510, pages 115–126, 1991.
R. Alur, C. Courcoubetis, and D. Dill. Model-checking in dense real-time. Information and Computation, 104(1):2–34, 1993. Preliminary version appears in the Proc. of 5th LICS, 1990.
R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994. Preliminary version appears in Proc. 17th ICALP, 1990, LNCS 443.
C. Baier. Personal communication, 1998.
C. Baier and M. Kwiatkowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11:125–155, 1998.
J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of UPPAAL. In Proceedings of the International Workshop on Software Tools for Technology Transfer, Aalborg, Denmark, July 1998.
A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Foundations of Software Technology and Theoretical Computer Science, volume 1026 of Lecture Notes in Computer Science, pages 499–513, 1995.
M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: a model-checking tool for real-time systems. In Proc. of the 10th Conference on Computer-Aided Verification, Vancouver, Canada, 28 June — 2 July 1998. Springer Verlag.
P. D’Argenio, J.-P. Katoen, T. Ruys, and J. Tretmans. Modeling and verifying a bounded retransmission protocol. In Z. Brezocnik and T. Kapus, editors, Proc. of COST 247 International Workshop on Applied Formal Methods in System Design, Maribor, Slovenia, Technical Report. University of Maribor, 1996.
H. Gregersen and H. E. Jensen. Formal design of reliable real time systems. Master’s thesis, Department of Mathematics and Computer Science, Aalborg University, 1995.
H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. Formal Aspects of Computing, 6(5):512–535, 1994.
T. Henzinger, P. Kopke, A. Puri, and P. Varaiya. What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94–124, Aug. 1998.
T. Henzinger and O. Kupferman. From quantity to quality. In O. Maler, editor, HART 97: Hybrid and Real-time Systems, Lecture Notes in Computer Science 1201, pages 48–62. Springer-Verlag, 1997.
T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994. Special issue for LICS 92.
G. Lafferriere, G. Pappas, and S. Yovine. Decidable hybrid systems. Technical Report UCB/ERL M98/39, University of California at Berkeley, June 1998.
S. Yovine. Model checking timed automata. In G. Rozenberg and F. Vaandrager, editors, Embedded Systems, volume 1494 of Lecture Notes in Computer Science. Springer, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kwiatkowska, M., Norman, G., Segala, R., Sproston, J. (1999). Automatic Verification of Real-Time Systems with Discrete Probability Distributions. In: Katoen, JP. (eds) Formal Methods for Real-Time and Probabilistic Systems. ARTS 1999. Lecture Notes in Computer Science, vol 1601. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48778-6_5
Download citation
DOI: https://doi.org/10.1007/3-540-48778-6_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66010-1
Online ISBN: 978-3-540-48778-4
eBook Packages: Springer Book Archive