Complex software systems typically involve features like time, concurrency and probability, where probabilistic com- putations play an increasing role. It is challenging to for- malize languages comprising all these features. We have proposed a language, which integrates probability with time and shared-variable concurrency. We also explored its op- erational semantics, where a set of algebraic laws has been investigated via bisimulation. In this paper, we consider the inverse work, the deriva- tion of operational semantics from algebraic semantics for our probabilistic language. This approach can be under- stood as the soundness investigation of operational seman- tics 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 determin- istic initially. This can model the execution of a program. Secondly we investigate the derivation of an operational se- mantics 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 sys- tem and the derivation strategy. This indicates the com- pleteness 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.
Citation:
Huibiao Zhu, Jifeng He, Jonathan P. Bowen, "Algebraic Approach to Operational Semantics and Observation-Oriented Semantics for a Timed Shared-Variable Language with Probability," sew, pp.131-143, 31st IEEE Software Engineering Workshop (SEW 2007), 2007