Operational semantics for product-form solution

TL;DR

This paper introduces a simplified stochastic process algebra inspired by PEPA, facilitating easier proofs of product-form solutions and analyzing how cooperation semantics affect their correctness.

Contribution

It presents a new simple process algebra that simplifies proof procedures for product-form solutions and examines the impact of cooperation semantics on their derivation.

Findings

Simplified process algebra enables easier proof of product-form solutions.

Cooperation semantics significantly influence the correctness of solutions.

Differences between the new algebra and PEPA are analyzed.

Abstract

In this paper we present product-form solutions from the point of view of stochastic process algebra. In previous work we have shown how to derive product-form solutions for a formalism called Labelled Markov Automata (LMA). LMA are very useful as their relation with the Continuous Time Markov Chains is very direct. The disadvantage of using LMA is that the proofs of properties are cumbersome. In fact, in LMA it is not possible to use the inductive structure of the language in a proof. In this paper we consider a simple stochastic process algebra that has the great advantage of simplifying the proofs. This simple language has been inspired by PEPA, however, detailed analysis of the semantics of cooperation will show the differences between the two formalisms. It will also be shown that the semantics of the cooperation in process algebra influences the correctness of the derivation of the product-form solutions.