Giving a net semantics to Markovian process algebra

We define two compositional net semantics for the stochastic process algebra Markovian process algebra (MPA), based on a class of stochastic Petri nets. The first semantics is operational in style and is defined by structural induction. We prove that both the functional and performance interleaving semantics are retrievable: given a process term E, the reachability graph and the Markov chain obtained from the net for E are the same as we obtain directly for E, according to MPA specification. Then, we present the other net semantics, which is defined in a denotational style. This additional semantics is proposed only to clarify that all the intended concurrency is expressed in the operational net model. Finally, we comment on an integrated specification strategy for concurrent systems, which is available also because of the operational net semantics described