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

摘要

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.