In this paper, we study behaviour descriptions with uncertain information such as “the probability of a system failure within a given time period is less than or equal to 0.3” in terms of process algebras. Typical systems that may show such behaviours include communicating systems with unreliable components, e.g. faulty medium. We present a process model for such behaviours, in which uncertain information is described by means of intervals of probabilities. In particular, we introduce a stochastic choice operator
i] Ei, where Φi's are intervals of probabilities. Roughly speaking, it is a process which may become Ei in one unit of time with a probability within the interval Φi. Such a process is considered as a specification specifying a set of processes with less uncertain information. We develop a notion of probabilistic simulation to order specifications in terms of the degree of uncertainty in the specifications, which generalize the notion of probabilistic bisimulation. A complete axiomatization for the induced congruence is provided.


Parallel Composition Atomic Action Probabilistic Process Uncertain Information Simulation Relation 
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. [BC83]
    G. Berry and L. Cosserat, The Synchronous Programming Language ESTEREL and its Mathematical Semantics, LNCS No. 197, 1983.Google Scholar
  2. [BBS92]
    J.C.M. Baeten, J.A. Bergstra and S.A. Smolka. Axiomatizing Probabilistic Processes: ACP with Generative Probabilities, in the proc. of CONCUR92, LNCS 630, 1992.Google Scholar
  3. [C90]
    I. Christoff, Testing Equivalence for Probabilistic Processes, Ph.D. Thesis, Uppsala University, Uppsala, Sweden, 1990.Google Scholar
  4. [CGL]
    Karlis Cerans, Jens Chr. Godskesen and Kim G. Larsen Time Modal Specification — Theory and Tools. Proceedings of the 5th Int. Conf. on Computer Aided Verificatio n, 1993.Google Scholar
  5. [G90]
    J.F. Groote, Specification and Verification of Real Time Systems in ACP, Report CS-R9015, CWI, Amsterdam, 1990, in the proceedings of PSTV X, 1990.Google Scholar
  6. [GSST90]
    R. van Glabbeek, S. A. Smolka, B. Steffen and C. Tofts, Reactive, Generative and Stratified Models of Probabilistic Processes, in the Proc. of LICS'90, 1990.Google Scholar
  7. [H88]
    M. Hennessy, Algebraic Theory of Processes, MIT press, 1988.Google Scholar
  8. [HJ90]
    H. Hansson and Bengt Jonsson, A Calculus for Communicating Systems with Time and Probability, in the Proc. of the 11'th IEEE Real Time Systems Symposium, 1990.Google Scholar
  9. [HR91]
    M. Hennessy and T. Regan, A Temporal Process Algebra, Technical Report 5/91, University of Sussex, 1991.Google Scholar
  10. [J91]
    A. Jeffrey, Linear Time Process Algebra, In the proc. of to CAV91, Aalborg University, Denmark.Google Scholar
  11. [JL91]
    B. Jonsson and K. G. Larsen, Specification and Refinement of Probabilistic Processes, LICS'91, Amsterdam, 1991.Google Scholar
  12. [JS90]
    C. Jou and S.A. Smolka, Equivalences, Congruences and Complete Axiomatizations for Probabilistic Processes, in the Proc. of CONCUR'90, LNCS 458, 1989.Google Scholar
  13. [L93]
    Gavin Lowe. Probabilities and Priorities in Timed CSP, Ph.D Thesis, Oxford, 1993.Google Scholar
  14. [LS89]
    K. G. Larsen and A. Skou, Bisimulation through Probabilistic Testing, in the Proc. of ACM POPL'89, 1989.Google Scholar
  15. [LS91]
    K. G. Larsen and A. Skou, Compositional Verification of Probabilistic Processes, in the proc. of CONCUR92, LNCS 630, 1992.Google Scholar
  16. [M80]
    R. Milner, A Calculus of Communicating Systems, LNCS 92, 1980.Google Scholar
  17. [M83]
    R. Milner, Calculi for Synchrony and Asynchrony, TCS, Vol 25, 1983.Google Scholar
  18. [M89]
    R. Milner, Communication and Concurrency, Prentice Hall, 1989.Google Scholar
  19. [MT90]
    F. Moller and C. Tofts, A Temporal Calculus of Communicating Systems, LNCS, No. 458, 1990.Google Scholar
  20. [N87]
    R. de Nicola, Extensional Equivalences For Transition Systems, Acta Informatia 24, 1987.Google Scholar
  21. [NH84]
    R. de Nicola and M. Hennessy, Testing equivalences for processes, TCS vol. 34, 1984.Google Scholar
  22. [RH89]
    W.P. de Roever and J.J.M. Hooman, Design and Verification of Real-time Distributed Computing: an Introduction to Compositional Methods, Proceeding of the 9th IFIP WG 6.1 International Symposium on Protocol Specification, Testing and Verification, 1989.Google Scholar
  23. [RR86]
    G.M. Reed and A.W. Roscoe, A Timed Model for Communicating Sequential Processes, LNCS, No. 226, 1986.Google Scholar
  24. [S90]
    J. Sifakis et al. The Algebra of Timed Processes ATP: Theory and Application, Laboratoire de Genie Informatique, IMAG-Campus, B.P.53X, 38041 Grenoble Cedex, France, December 1990, in M. Broy and C.B. Jones, Programming Concepts and Methods, 1990.Google Scholar
  25. [W91]
    Wang Yi, CCS + Time = an Interleaving Model for Real Time Systems, in the Proc. of ICALP'91, LNCS No. 510.Google Scholar
  26. [W92]
    Wang Yi and Kim G Larsen, Testing Nondeterministic and Probabilistic Processes, in the Proc. of the 12th IFIP International Symposium on Protocol Specification, Testing and Verification, Florida, USA, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1994

Authors and Affiliations

  • Wang Yi
    • 1
  1. 1.Department of Computer SystemsUppsala UniversityUppsalaSweden

Personalised recommendations