Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language

Huibiao Zhu, Fan Yang, Jifeng He, Jonathan P. Bowen, Jeff W. Sanders, Shengchao Qin

    Research output: Contribution to journalArticle

    Abstract

    Complex software systems typically involve features like time, concurrency and probability, with probabilistic computations playing an increasing role. However, it is currently challenging to formalize languages incorporating all those features. Recently, the language PTSC has been proposed to integrate probability and time with shared-variable concurrency (Zhu et al. (2006, 2009) [51], [53]), where the operational semantics has been explored and a set of algebraic laws has been investigated via bisimulation. This paper investigates the link between the operational and algebraic semantics of PTSC, highlighting both its theoretical and practical aspects.

    The link is obtained by deriving the operational semantics from the algebraic semantics, an approach that may be understood as establishing soundness of the operational semantics with respect to the algebraic semantics. Algebraic laws are provided that suffice to convert any PTSC program into a form consisting of a guarded choice or an internal choice between programs, which are initially deterministic. That form corresponds to a simple execution of the program, so it is used as a basis for an operational semantics. In that way, the operational semantics is derived from the algebraic semantics, with transition rules resulting from the derivation strategy. In fact the derived transition rules and the derivation strategy are shown to be equivalent, which may be understood as establishing completeness of the operational semantics with respect to the algebraic semantics.

    That theoretical approach to the link is complemented by a practical one, which animates the link using Prolog. The link between the two semantics proceeds via head normal form. Firstly, the generation of head normal form is explored, in particular animating the expansion laws for probabilistic interleaving. Then the derivation of the operational semantics is animated using a strategy that exploits head normal form. The operational semantics is also animated. These animations, which again supports to claim soundness and completeness of the operational semantics with respect to the algebraic, are interesting because they provide a practical demonstration of the theoretical results.
    Original languageEnglish
    Pages (from-to)2-25
    JournalJournal of Logic and Algebraic Programming
    Volume81
    Issue number1
    DOIs
    Publication statusPublished - 2012

    Fingerprint Dive into the research topics of 'Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language'. Together they form a unique fingerprint.

  • Cite this