Denotational Semantics for a Probabilistic Timed Shared-Variable Language

  • Huibiao Zhu
  • Jeff W. Sanders
  • Jifeng He
  • Shengchao Qin
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7681)


Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. We have proposed a language, which integrates probability with time and shared-variable concurrency (called PTSC [19]). We also explored its operational semantics, where a set of algebraic laws has been investigated via bisimulation.

In this paper we explore the denotational semantics for our probabilistic language. In order to deal with the above three features and the nondeterminism, we introduce a tree structure, called P-tree, to model concurrent probabilistic programs. The denotational semantics of each statement is formalized in the structure of P-tree. Based on the achieved semantics, a set of algebraic laws is explored; i.e., especially those parallel expansion laws. These laws can be proved via our achieved denotational semantics.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    den Hartog, J.: Probabilistic Extensions of Semantic Models. PhD thesis, Vrije University, The Netherlands (2002)Google Scholar
  2. 2.
    den Hartog, J., de Vink, E.: Mixing up nondeteminism and probability: A premliminary report. Electronic Notes in Theoretical Computer Science 22 (1999)Google Scholar
  3. 3.
    den Hartog, J., de Vink, E., de Bakker, J.: Metric semantics and full abstractness for action refinement and probabilistic choice. Electronic Notes in Theoretical Computer Science 40 (2001)Google Scholar
  4. 4.
    He, J.: Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers. The McGraw-Hill International Series in Software Engineering (1994)Google Scholar
  5. 5.
    He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Science of Computer Programming 28(2-3), 171–192 (1997)MathSciNetzbMATHCrossRefGoogle Scholar
  6. 6.
    He, J., Zhu, H.: Formalising Verilog. In: Proc. ICECS 2000: IEEE International Conference on Electronics, Circuits and Systems, pp. 412–415. IEEE Computer Society Press (December 2000)Google Scholar
  7. 7.
    Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)Google Scholar
  8. 8.
    McIver, A., Morgan, C.: Partial correctness for probabilistic demonic programs. Theoretical Computer Science 266(1-2), 513–541 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  9. 9.
    McIver, A., Morgan, C.: Abstraction, Refinement and Proof of Probability Systems. Monographs in Computer Science. Springer (October 2004)Google Scholar
  10. 10.
    McIver, A., Morgan, C., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)CrossRefGoogle Scholar
  11. 11.
    Ndukwu, U., Sanders, J.W.: Reason about a distributed probabilistic system. Technical Report 401, UNU/IIST, P.O. Box 3058, Macau SAR, China (August. 2008)Google Scholar
  12. 12.
    Nissanke, N.: Realtime Systems. Prentice Hall International Series in Computer Science (1997)Google Scholar
  13. 13.
    Núñez, M.: Algebraic theory of probabilistic processes. The Journal of Logic and Algebraic Programming 56, 117–177 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Núñez, M., de Frutos-Escrig, D.: Testing semantics for probabilistic LOTOS. In: Proc FORTE 1995: IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada. IFIP Conference Proceedings, vol. 43, pp. 367–382. Chapman and Hall (1996)Google Scholar
  15. 15.
    Núñez, M., de Frutos-Escrig, D., Díaz, L.F.L.: Acceptance Trees for Probabilistic Processes. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 249–263. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  16. 16.
    Park, S., Pfenning, F., Thrun, S.: A probabilistic language based upon sampling functions. In: Proc. POPL 2005: 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 171–182. ACM (January 2005)Google Scholar
  17. 17.
    Zhu, H.: Linking the Semantics of a Multithreaded Discrete Event Simulation Language. PhD thesis, London South Bank University (February 2005)Google Scholar
  18. 18.
    Zhu, H., He, J., Bowen, J.P.: From algebraic semantics to denotational semantics for verilog. Innovations in Systems and Software Engineering: A NASA Journal 4(4), 341–360 (2008)CrossRefGoogle Scholar
  19. 19.
    Zhu, H., Qin, S., He, J., Bowen, J.P.: PTSC: probability, time and shared-variable concurrency. Innovations in Systems and Software Engineering: A NASA Journal 5(4), 271–284 (2009)CrossRefGoogle Scholar
  20. 20.
    Zhu, H., Yang, F., He, J., Bowen, J.P., Sanders, J.W., Qin, S.: Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language. J. Log. Algebr. Program. 81(1), 2–25 (2012)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Huibiao Zhu
    • 1
  • Jeff W. Sanders
    • 2
  • Jifeng He
    • 1
  • Shengchao Qin
    • 3
  1. 1.Shanghai Key Laboratory of Trustworthy Computing Software Engineering InstituteEast China Normal UniversityShanghaiChina
  2. 2.African Institute for Mathematical SciencesMuizenbergSouth Africa
  3. 3.School of ComputingUniversity of TeessideMiddlesbroughUK

Personalised recommendations