Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
- Speaker: Prof Huibiao Zhu (East China Normal University)
- Host: Richard Banach
- 2nd May 2012 at 14:15 in Lecture Theatre 1.4, Kilburn Building
Recently, the language PTSC has been proposed to integrate probability and time with shared-variable concurrency (Zhu et al. ). This talk considers the link between the operational semantics and algebraic semantics for PTSC. Our investigation includes both the theoretical and practical approaches to the link. For aiming the link, we consider 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. 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. Besides the above theoretical approach to the link, we also study the practical approach to the link. We consider the animation of the link between operational semantics and algebraic semantics for PTSC.