In: IEEE Computer Soc. Press, Proc. of 6th International Workshop on Petri Nets and Performance Models - PNPM'95, Durham, N. Carolina, USA, pages 169-178. 1995.
Abstract: In this paper we define two compositional net semantics for the stochastic process algebra Markovian Process Algeb ra (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 Maarkov 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 here.