Composing Systems While Preserving Probabilities

  • Sonja Georgievska
  • Suzana Andova
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6342)


Restricting the power of the schedulers that resolve the nondeterminism in probabilistic concurrent systems has recently drawn the attention of the research community. The goal is to preserve the probabilistic behaviour of systems when composed, and at the same time, to guarantee compositionality for trace-like equivalences. In our previous work, we have defined a model of probabilistic systems with labels on the internal transitions, that restrict the power of the schedulers. A trace-style equivalence for the same model, compatible with a synchronous parallel composition, was proposed. In the present paper we generalize the parallel composition to allow for action interleaving and synchronization on a given set of actions, combined with hiding afterwards. We propose a method for automatic labeling of the internal transitions that arise due to the parallel composition. These labels reflect the information that the components use in order to resolve the nondeterminism in the composition, and thus restrict the power of the schedulers. We show that our equivalence is compositional w.r.t. the parallel composition. We also define operational semantics that, besides the parallel composition, includes deadlock, and four types of choices – action, external, internal, and probabilistic.


Operational Semantic Internal Transition Probabilistic Choice Parallel Composition Process Algebra 
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.
    Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Ready-trace semantics for concrete process algebra with the priority operator. The Computer Journal 30(6), 498–506 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Cazorla, D., Cuartero, F., Valero, V., Pelayo, F.L., Pardo, J.J.: Algebraic theory of probabilistic and nondeterministic processes. Journal of Logic and Algebraic Programming 55(1-2), 57–103 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Chatzikokolakis, K., Palamidessi, C.: Making random choices invisible to the scheduler. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 42–58. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
    Cheung, L., Lynch, N., Segala, R., Vaandrager, F.: Switched PIOA: Parallel composition via distributed scheduling. Theoret. Comp. Science 365(1-2), 83–108 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    de Alfaro, L., Henzinger, T., Jhala, R.: Compositional methods for probabilistic systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 351–365. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  6. 6.
    Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.: Characterising testing preorders for finite probabilistic processes. Logical Methods in Computer Science 4(4:4), 1–33 (2008)MathSciNetzbMATHGoogle Scholar
  7. 7.
    Georgievska, S., Andova, S.: Retaining the probabilities in probabilistic testing theory. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 79–93. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  8. 8.
    Georgievska, S., Andova, S.: Process theory for probabilistic ready-trace equivalence. Technical Report (2010),
  9. 9.
    Giro, S., D’Argenio, P.: On the expressive power of schedulers in distributed probabilistic systems. In: Proc. QAPL 2009. ENTCS, vol. 253(3), pp. 45–71 (2009)Google Scholar
  10. 10.
    van Glabbeek, R.J.: The linear time – branching time spectrum I; The semantics of concrete, sequential processes. In: Handbook of Process Algebra, ch. 1, pp. 3–99. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  11. 11.
    Hansson, H.A.: Time and Probability in Formal Design of Distributed Systems. Elsevier, Amsterdam (1994)Google Scholar
  12. 12.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  13. 13.
    Kwiatkowska, M.Z., Norman, G.J.: A fully abstract metric-space denotational semantics for reactive probabilistic processes. In: Proc. COMPROX 1998. ENTCS, vol. 13 (1998)Google Scholar
  14. 14.
    Lindley, D.V.: Introduction to Probability and Statistics from a Bayesian Viewpoint. Cambridge University Press, Cambridge (1980)zbMATHGoogle Scholar
  15. 15.
    Lowe, G.: Representing nondeterministic and probabilistic behaviour in reactive processes. Technical Report PRG-TR-11-93. Oxford Univ. Comp. Labs (1993)Google Scholar
  16. 16.
    Lynch, N., Segala, R., Vaandrager, F.: Observing branching structure through probabilistic contexts. SIAM Journal on Computing 37(4), 977–1013 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1982)zbMATHGoogle Scholar
  18. 18.
    Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Aspects of Computing 8(6), 617–647 (1996)CrossRefzbMATHGoogle Scholar
  19. 19.
    Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  20. 20.
    Segala, R.: Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT (1995)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Sonja Georgievska
    • 1
  • Suzana Andova
    • 1
  1. 1.Department of Mathematics and Computer ScienceEindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations