Stochastic semantics for Communicating Piecewise Deterministic Markov Processes

CPDPs (Communicating Piecewise Deterministic Markov Processes) can be used for compositional specification of systems from the class of stochastic hybrid processes formed by PDPs (Piecewise Deterministic Markov Processes). We give an extension of the CPDP model of [6]. This extension provides richer interaction possibilities such as broadcasting (and recieving) of multiple signals at the same time. We show that the |P A| operator from [7] can be used in the context of CPDPs to express all these interactions. We provide an algorithm in which scheduling and maximal progress are used to find the PDP that models the behavior of a CPDP of this new type. We give the conditions under which a CPDP allows this PDP-semantics.