FuTS - A Uniform Framework for the Definition of Stochastic Process Languages

Day - Time: 07 October 2011, h.11:00
Place: Area della Ricerca CNR di Pisa - Room: C-29

Maurice Henri ter Beek


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 talk 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,α,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 α. The FuTSs framework is used to model represenative 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 talk, first the FuTSs are introduced and then the semantics for a simple language used to directly describe (unlabeled) CTMCs.