De Nicola R., Latella D., Loreti M., Massink M. State to function labelled transition systems: a uniform framework for defining stochastic process calculi. Technical report, 2011. |

Abstract (English) |
Process Algebras are one of the most successful formalisms for modeling concurrent systems and proving their properties. Due to the growing interest in the analysis of shared-resource systems, stochastic process algebras have received great attention. The main aim has been the integration of qualitative descriptions with quantitative (especially performance) ones in a single mathematical framework by building on the combination of Labeled Transition Systems and Continuous-Time Markov Chains. In this paper a unifying framework is introduced for providing the semantics of some of the most representative stochastic process languages; aiming at a systematic understanding of their similarities and differences. The used unifying framework is based on so called State to Function Labelled Transition Systems, FuTSs for short, that are state-transition structures where each transition is a triple of the form $(s,a,P)$. The first and the second components are the source state and the label of the transition while the third component, P, is the continuation function associating a value of a suitable type to each state s'. A non-zero value may represent the cost to reach s' from s via a. The FuTSs framework is used to model representative fragments of major stochastic process calculi and the costs of continuation function do represent the rate of the exponential distribution characterizing the execution time of the performed action. In the paper, first the semantics for a simple language used to directly describe (unlabeled) CTMCs is provided, then a number of calculi that permit parallel composition of models according to the two main communication paradigms (multiparty and binary synchronization) are considered. Finally, languages where actions and rates are kept separated are modeled and the issues related to co-existence of stochastic and nondeterministic behaviors are discussed. For each calculus, the formal correspondence between the FuTSs semantics and its original SOS based semantics is established. | |

Subject | Continuous Time Markov Chains Stochastic Process Calculi Structured Operational Semantics H.1 MODELS AND PRINCIPLES F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES 68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

1) Download Document PDF |

Open access Restricted Private