Reduction Semantics in Markovian Process Algebra With and Without Durational Actions

Stochastic (Markovian) process algebras in the literature have been defined in very simple settings where it is not possible to readjust parallel processes during the inference of their transitions, i.e. to represent their evolution by (unlabeled) reduction transitions. Technically, this is due to limitations in existing approaches to stochastic operational semantics that make inference not compatible with a structural congruence relation that, e.g., enacts commutative and associative properties of parallel. This has the main drawback that when we want to introduce stochastic durations in a process algebra whose semantics is already defined in reduction style (a quite common practice for non-basic languages) we have to modify the style of the semantics. We introduce a new technique that allows us to define semantics for Markovian process algebra when structural congruence is used for inferring transitions. As application examples, we define the reduction semantics of Markovian versions of the pi-calculus, considering both the cases of Markovian durations: being additional standalone prefixes and being, instead, associated to standard (synchronized) actions, giving them a duration. In both cases we show the obtained reduction semantics to be correct with respect to the standard Markovian one (defined in labeled operational semantics style) by providing a Markovian extension of classical pi-calculus Harmony theorem. Finally, we show that our technique allows us to obtain a "natural" associative semantics for parallel in the context of stochastic pi-calculus, differently from the original non-associative semantics.