Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
den Hartog, J.: Probabilistic Extensions of Semantic Models. PhD thesis, Vrije University, The Netherlands (2002)
den Hartog, J., de Vink, E.: Mixing up nondeteminism and probability: A premliminary report. Electronic Notes in Theoretical Computer Science 22 (1999)
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)
He, J.: Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers. The McGraw-Hill International Series in Software Engineering (1994)
He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Science of Computer Programming 28(2-3), 171–192 (1997)
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)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)
McIver, A., Morgan, C.: Partial correctness for probabilistic demonic programs. Theoretical Computer Science 266(1-2), 513–541 (2001)
McIver, A., Morgan, C.: Abstraction, Refinement and Proof of Probability Systems. Monographs in Computer Science. Springer (October 2004)
McIver, A., Morgan, C., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)
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)
Nissanke, N.: Realtime Systems. Prentice Hall International Series in Computer Science (1997)
Núñez, M.: Algebraic theory of probabilistic processes. The Journal of Logic and Algebraic Programming 56, 117–177 (2003)
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)
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)
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)
Zhu, H.: Linking the Semantics of a Multithreaded Discrete Event Simulation Language. PhD thesis, London South Bank University (February 2005)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhu, H., Sanders, J.W., He, J., Qin, S. (2013). Denotational Semantics for a Probabilistic Timed Shared-Variable Language. In: Wolff, B., Gaudel, MC., Feliachi, A. (eds) Unifying Theories of Programming. UTP 2012. Lecture Notes in Computer Science, vol 7681. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35705-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-35705-3_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35704-6
Online ISBN: 978-3-642-35705-3
eBook Packages: Computer ScienceComputer Science (R0)