Algebraic approach to operational semantics and observation-oriented semantics for a timed shared-variable language with probability

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. We also explored its operational semantics, where a set of algebraic laws has been investigated via bisimulation. In this paper, we consider the inverse work, the derivation of operational semantics from algebraic semantics for our probabilistic language. This approach can be understood as the soundness investigation of operational semantics from the viewpoint of algebraic semantics. Firstly we present the algebraic laws for our probabilistic language. Every program can be expressed as either a guarded choice, or the summation of a set of processes which are deterministic initially. This can model the execution of a program. Secondly we investigate the derivation of an operational semantics from its algebraic semantics. A set of transition rules are derived from the given derivation strategy. Thirdly we explore the equivalence of the derived transition system and the derivation strategy. This indicates the completeness of our operational semantics from the viewpoint of algebraic semantics. Meanwhile, we also investigate the observation-oriented semantic model and its derivation from algebraic semantics.