Modeling and Analyzing Concurrent Systems with MPA

Process algebras are one of the main tools for modeling and analyzing concurrent systems. However, they can be used to describe only the functional aspect of system behavior. Recently, the relevance of integrating performance evaluation within the process of specification, design and implementation of concurrent systems has been widely recognized. Hence, an effort has been made in order to handle also the temporal aspect of system behavior. In this paper the stochastic process algebra MPA (Markovian Process Algebra) is briefly introduced, together with its operational interleaving semantics, its markovian semantics and its operational net semantics. A concurrent system is described as a term of MPA. The operational interleaving semantics (defined by following Plotkin's structured operational semantics approach, augmented with two transformations) associates a labeled transition system with each MPA term. The markovian semantics is defined through an algorithm which transforms labeled transition systems into state transition rate diagrams of homogeneous continuous time Markov chains. The operational net semantics is defined by following an extension of Plotkin's structured operational semantics approach to nets (as proposed by Degano-De Nicola-Montanari and Olderog), yielding a generalized stochastic Petri net. A modeling technique for concurrent systems based on MPA is also proposed which integrates different points of view of concurrent systems as well as the qualitative and quantitative analysis of concurrent systems. Finally, some examples are shown which demonstrate the expressiveness and the compositionality of MPA.