Denotational Semantics for a Probabilistic Timed Shared-Variable Language
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 ). 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.
- 1.den Hartog, J.: Probabilistic Extensions of Semantic Models. PhD thesis, Vrije University, The Netherlands (2002)Google Scholar
- 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.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.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
- 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.Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)Google Scholar
- 9.McIver, A., Morgan, C.: Abstraction, Refinement and Proof of Probability Systems. Monographs in Computer Science. Springer (October 2004)Google Scholar
- 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.Nissanke, N.: Realtime Systems. Prentice Hall International Series in Computer Science (1997)Google Scholar
- 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
- 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.Zhu, H.: Linking the Semantics of a Multithreaded Discrete Event Simulation Language. PhD thesis, London South Bank University (February 2005)Google Scholar