Composition and Refinement of Probabilistic Real-Time Systems

  • Zhiming Liu
  • Jens Nordahl
  • Erling Vagn Sørensen
Conference paper


In this paper we illustrate, by way of examples, composition, analysis and refinement of systems modelled by means of probabilistic automata behaving as Markov chains over discrete time. For a formalised and general treatment of these ideas the reader is referred to [6].


Parallel Composition Matrix Expression Probability Matrice Primitive State State Flame 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    A.P.Ravn, H.Rischel, and K.M.Hansen. Specifying and verifying requirements of real-time systems. IEEE Trans. Software Eng., 19(1), 1993.Google Scholar
  2. 2.
    J.C.M. Baeten, J.A. Bergstra, and S.A. Smolka. Axiomatizing probabilistic processes: Acp with generative probabilities. In Lecture Notes in Computer Science, volume 630, pages 472–485. Springer Verlag, 1992.Google Scholar
  3. 3.
    B. Jonsson and K. Larsen. Specification and refinement of probabilistic processes. In Proc. 6th Annual Symp. on Logics in Computer Science, pages 226–277, 1991.Google Scholar
  4. 4.
    K. G. Larsen and A. Skou. Compositional verification of probabilistic processes. In Lecture Notes in Computer Science, volume 630, pages 456–471. Springer Verlag, 1992.Google Scholar
  5. 5.
    Z. Liu, E.V. Sørensen, A.P. Ravn, and C.C. Zhou. Towards a calculus of systems dependability. Technical report, Department of Computer Science, Technical University of Demark, 1993. To appear in Journal of High Integrity Systems, Oxford University Press.Google Scholar
  6. 6.
    Zhiming Liu, J. Nordahl, and E. V. Sørensen. Compositional design and refinement of probabilistic real time systems. Technical report, Institute of Computer Science, Technical University of Denmark, DK-2800 Lyngby, Denmark, 1993.Google Scholar
  7. 7.
    C.C. Zhou, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1992.MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag London Limited 1993

Authors and Affiliations

  • Zhiming Liu
    • 1
  • Jens Nordahl
    • 2
  • Erling Vagn Sørensen
    • 2
  1. 1.Department of Computer ScienceUniversity of WarwickEngland
  2. 2.Department of Computer ScienceTechnical University of DenmarkDenmark

Personalised recommendations