Model-checking continuous-time Markov chains

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.

REFERENCES

• 1: ALUR, R., COUCOUBETIS, C., AND DILL, D. L. 1990. Model checking for real-time systems. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science, IEEE Press, Piscataway, NJ, 414-425.
• 2: Rajeev Alur , Costas Courcoubetis , David Dill, Model-checking for probabilistic real-time systems (extended abstract), Proceedings of the 18th international colloquium on Automata, languages and programming, p.115-126, June 1991, Madrid, Spain
• 3: Christel Baier , Joost-Pieter Katoen , Holger Hermanns, Approximate Symbolic Model Checking of Continuous-Time Markov Chains, Proceedings of the 10th International Conference on Concurrency Theory, p.146-161, August 24-27, 1999
• 4: COURCOUBETIS, C. AND YANNAKAKIS, M. 1988. Verifying temporal properties of finite state probabilistic programs. In Proceedings of the IEEE Conference on Decision and Control, IEEE Press, Piscataway, NJ, 338-345.
• 5: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 6: EWING, J. H. 1991. Numbers. Springer-Verlag, Vienna, Austria.
• 7: HANSSON, H. AND JONSSON, B. 1994. A logic for reasoning about time and reliability. Form. Asp. Comput. 6, 512-535.
• 8: KALIATH, T. 1980. Linear Systems. Prentice-Hall, New York, NY.
• 9: NIVEN, I. 1956. Irrational Numbers. John Wiley and Sons Ltd., Chichester, UK.
• 10: Daniel Richardson, How to recognize zero, Journal of Symbolic Computation, v.24 n.6, p.627-645, Dec. 1997 [doi>10.1006/jsco.1997.0157]
• 11: Ross, S. 1983. Stochastic Processes. John Wiley and Sons Ltd., Chichester, UK.
• 12: TARSKI, A. 1951. A Decision Procedure for Elementary Algebra and Geometry. University of California Press, Berkeley, CA.
• 13: WILKIE, A. J. 1995. On the decidability of the real exponential field. In Proceedings of the Conference on Order in Algebra and Logic (Oxford, UK),

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.5 Roots of Nonlinear Equations
          Subjects: Systems of equations
  G.3 PROBABILITY AND STATISTICS
      Subjects: Stochastic processes

General Terms:
Theory, Verification

Keywords:
formal verification, model checking, real time, transcendental number theory