Abstract
We present a logical formalism for expressing properties of continuous time Markov chains. The semantics for such properties arise as a natural extension of previous work on discrete time Markov chains to continuous time. The major result is that the verification problem is decidable; this is shown using results in algebraic and transcendental number theory.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, C. Courcoubetis, and D. Dill. Model Checking for Real-Time Systems. In Proc. IEEE Symposium on Logic in Computer Science, pages 414–425, 1990.
R. Alur, C. Courcoubetis, and D. Dill. Model Checking for Probabilistic Real Time Systems. In Proc. of the Colloquium on Automata, Languages, and Programming, pages 115–126, 1991.
C. Courcoubetis and M. Yannakakis. Verifying Temporal Properties of Finite State Probabilistic Programs. In Proc. IEEE Symposium on the Foundations of Computer Science, pages 338–345, 1988.
E. A. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science, pages 996–1072. Elsevier Science, 1990.
J. H. Ewing. Numbers. Springer-Verlag, 1991.
H. Hansson and B. Jonsson. A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing, 6:512–535, 1994.
T. Kaliath. Linear Systems. Prentice-Hall, 1980.
I. Niven. Irrational Numbers. John-Wiley, 1956.
S. Ross. Stochastic Processes. Wiley, 1983.
H. L. Royden. Real Analysis. Macmillan Publishing, 1989.
A. Tarski. A Decision Procedure for Elementary Algebra and Geometry. University of California Press, 1951.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aziz, A., Sanwal, K., Singhal, V., Brayton, R. (1996). Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_75
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_75
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive