Denotational Semantics for a Probabilistic Timed Shared-Variable Language

Huibiao Zhu, Jeff W. Sanders, Jifeng He, Shengchao Qin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    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.
    Original languageEnglish
    Title of host publicationUnifying Theories of Programming, UTP 2012
    EditorsB. Wolff , M. C. Gaudel , A. Feliachi
    PublisherSpringer Berlin
    ISBN (Electronic)9783642357053
    ISBN (Print)9783642357046
    Publication statusPublished - 2012
    EventUnifying Theories of Programming, 4th International Symposium - Paris, France
    Duration: 27 Aug 201228 Aug 2012
    Conference number: 4

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer, Berlin


    ConferenceUnifying Theories of Programming, 4th International Symposium
    Abbreviated titleUTP 2012


    Dive into the research topics of 'Denotational Semantics for a Probabilistic Timed Shared-Variable Language'. Together they form a unique fingerprint.

    Cite this