Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Model-checking for probabilistic real-time systems

  • Specification And Verification (Session 3)
  • Conference paper
  • First Online:

Part of the book series:Lecture Notes in Computer Science ((LNCS,volume 510))

Included in the following conference series:

Abstract

Model-checking is a method of verifying concurrent systems in which a state-graph model of the system behavior is compared with a temporal logic formula. This paper extends model-checking to stochastic real-time systems, whose behavior depends on probabilistic choice and quantitative time. The specification language isTCTL, a branching-time temporal logic for expressing real-time properties. We interpret the formulas of the logic over generalized semi-Markov processes. Our model can express constraints like “the delay between the request and the response is distributed uniformly between 2 to 4 seconds”.

We present an algorithm that combines model-checking for real-time non-probabilistic systems with model-checking for finite-state discrete-time Markov chains. The correctness of the algorithm is not obvious, because it analyzes the projection of a Markov process onto a finite state space. The projection process is not Markov, so our most significant result is that the model-checking algorithm works.

(Extended abstract)

Supported by ESPRIT BRA project SPEC

Supported by the NSF under grant MIP-8858807.

This is a preview of subscription content,log in via an institution to check access.

Access this chapter

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. R. Alur, C. Courcoubetis, D. Dill, “Model-checking for real-time systems,” 5th LICS, 1990.

    Google Scholar 

  2. R. Alur, D.L. Dill, “Automata for modeling real-time systems,” 17th ICALP, InLecture Notes in Computer Science,443, 1990.

    Google Scholar 

  3. R. Alur, T.A. Henzinger, “A really temporal logic,” 29th FOCS, 1989.

    Google Scholar 

  4. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, L.J. Hwang, “Symbolic modelchecking: 1020 states and beyond,” 5th LICS, 1990.

    Google Scholar 

  5. E.M. Clarke, E.A. Emerson, A.P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” ACMTOPLAS8(2), 1986.

    Google Scholar 

  6. C. Courcoubetis, M. Yannakakis, “Verifying temporal properties of finite-state probabilistic programs,” 29th FOCS, 1988.

    Google Scholar 

  7. E.A. Emerson, E.C. Clarke, “Using branching time temporal logic to synthesize synchronization skeletons,”Science of Computer Programming2, 1982.

    Google Scholar 

  8. P. Godefroid, “Using partial orders to improve automatic verification methods,” InProceedings of Workshop on Computer Aided Verification, Rutgers, 1990.

    Google Scholar 

  9. H. Hansson, B. Jonsson, “A Framework for Reasoning about Time and Reliability,” Real Time Systems Symposium, 1989.

    Google Scholar 

  10. R. Koymans, “Specifying message passing and time-critical systems with temporal logic,” Ph.D. Thesis, Eindhoven Univ. of Tech., 1989.

    Google Scholar 

  11. H.R. Lewis, “A logic of concrete time intervals,” 5th LICS, 1990.

    Google Scholar 

  12. D. Lehman, S. Shelah, “Reasoning with time and chance,”Information and Control53, 1982.

    Google Scholar 

  13. A. Pnueli, L. Zuck, “Probabilistic verification by tableaux,” 1st LICS, 1986.

    Google Scholar 

  14. G.S. Shedler,Regeneration and Networks of Queues, Springer-Verlag, 1987.

    Google Scholar 

  15. W. Whitt, “Continuity of generalized semi-Markov processes,”Math. Oper. Res.5,1980.

    Google Scholar 

  16. M. Vardi, “Automatic verification of probabilistic concurrent finite-state programs,” 26th STOC, 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Stanford University, USA

    Rajeev Alur & David Dill

  2. Computer Science Inst, FORTH and Computer Science Dept, University of Crete, Greece

    Costas Courcoubetis

Authors
  1. Rajeev Alur

    You can also search for this author inPubMed Google Scholar

  2. Costas Courcoubetis

    You can also search for this author inPubMed Google Scholar

  3. David Dill

    You can also search for this author inPubMed Google Scholar

Editor information

Javier Leach Albert Burkhard Monien Mario Rodríguez Artalejo

Rights and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Alur, R., Courcoubetis, C., Dill, D. (1991). Model-checking for probabilistic real-time systems. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds) Automata, Languages and Programming. ICALP 1991. Lecture Notes in Computer Science, vol 510. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54233-7_128

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp