Product-forms for Probabilistic Input/Output Automata

Probabilistic I/O automata (PIOAs) provide a modelling framework that is well suited for describing and analyzing distributed and concurrent systems. They incorporate a notion of probabilistic choice as well as a notion of composition that allows one to construct a PIOA for a composite system from a collection of simpler PIOAs representing the components. Differently from other probabilistic models, the local actions of a PIOA are associated with time delays governed by independent random variables with continuous-time exponential distributions. The contribution of this paper consists in studying the product-form property for PIOAs. Our main result is the formulation of a theorem giving sufficient conditions for a composition of PIOAs to be in product-form and hence to efficiently compute its stationary probabilities.