Expressing Processes with Different Action Durations through Probabilities

  • Mario Bravetti
  • Alessandro Aldini
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2165)


We consider a discrete time process algebra capable of (i) modeling processes with different probabilistic advancing speeds (mean number of actions executed per time unit), and (ii) expressing probabilistic external/internal choices and multiway synchronization. We show that, when evaluating steady state based performance measures expressed by associating rewards with actions, such a probabilistic approach provides an exact solution even if advancing speeds are considered not to be probabilistic (i.e. actions of different processes have a different exact duration), without incurring in the state space explosion problem which arises with an intuitive application of a standard synchronous approach. We then present a case study on multi-path routing showing the expressiveness of our calculus and that it makes it particularly easy to produce scalable specifications.


Reactive Action Action Frequency Action Duration Parallel Composition Reward Structure 
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. Aldini, M. Bravetti, “An Asynchronous Calculus for Generative-Reactive Probabilistic Systems”, in Proc. of 8th Int. Workshop on Process Algebra and Performance Modeling, pp. 591–605, 2000Google Scholar
  2. 2.
    M. Bravetti, A. Aldini, “An Asynchronous Calculus for Generative-Reactive Probabilistic Systems”, Tech. Rep. UBLCS-2000-03, Univ. Bologna, Italy, 2000Google Scholar
  3. 3.
    J.C.M. Baeten, J.A. Bergstra, S.A. Smolka, “Axiomatizing Probabilistic Processes: ACP with Generative Probabilities”, in Inf. and Comp. 121:234–255, 1995zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    M. Bernardo, “Theory and Application of Extended Markovian Process Algebra”, Ph. D. Thesis, Univ. Bologna, Italy, 1999Google Scholar
  5. 5.
    R.J. van Glabbeek, S.A. Smolka, B. Steffen, “Reactive, Generative and Stratified Models of Probabilistic Processes”, in Inf. and Comp. 121:59–80, 1995zbMATHCrossRefGoogle Scholar
  6. 6.
    C.A.R. Hoare, “Communicating Sequential Processes”, Prentice Hall, 1985Google Scholar
  7. 7.
    C.-C. Jou, S.A. Smolka, “Equivalences, Congruences, and Complete Axiomatizations for Probabilistic Processes”, in Proc. of 1st Int. Conf. on Concurrency Theory, LNCS 458:367–383, 1990Google Scholar
  8. 8.
    K.G. Larsen, A. Skou, “Compositional Verification of Probabilistic Processes”, in Proc. of 3rd Int. Conf. on Concurrency Theory, LNCS 630:456–471, 1992Google Scholar
  9. 9.
    R. Segala, “Modeling and Verification of Randomized Distributed Real-Time Systems”, Ph. D. Thesis, MIT, Boston (MA), 1995Google Scholar
  10. 10.
    A. S. Tanenbaum, “Computer Networks”, Prentice Hall, 1996Google Scholar
  11. 11.
    C. Tofts, “Processes with Probabilities, Priority and Time”, in Formal Aspects of Computing 6:536–564, 1994zbMATHCrossRefGoogle Scholar
  12. 12.
    S. H. Wu, S.A. Smolka, E.W. Stark, “Composition and Behaviors of Probabilistic I/O Automata”, in Theoretical Computer Science 176:1–38, 1997zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Mario Bravetti
    • 1
  • Alessandro Aldini
    • 1
  1. 1.Dipartimento di Scienze dell’InformazioneUniversità di BolognaBolognaItaly

Personalised recommendations