TY - GEN
T1 - Denotational semantics for a probabilistic timed shared-variable language
AU - Zhu, Huibiao
AU - Sanders, Jeff W.
AU - He, Jifeng
AU - Qin, Shengchao
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84893719300
U2 - 10.1007/978-3-642-35705-3_11
DO - 10.1007/978-3-642-35705-3_11
M3 - 会议稿件
AN - SCOPUS:84893719300
SN - 9783642357046
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 224
EP - 247
BT - Unifying Theories of Programming - 4th International Symposium, UTP 2012, Revised Selected Papers
T2 - 4th International Symposium on Unifying Theories of Programming, UTP 2012
Y2 - 27 August 2012 through 28 August 2012
ER -