Compositional analysis of expected delays in networks of probabilistic I/O automata

Probabilistic I/O automata (PIOA) constitute a model for distributed or concurrent systems that incorporates a notion of probabilistic choice. The PIOA model provides a notion of composition, for constructing a PIOA for a composite system from a collection of PIOAs representing the components. We present a method for computing completion probability and expected completion time for PIOAs. Our method is compositional, in the sense that it can be applied to a system of PIOAs, one component at a time, without ever calculating the global state space of the system (i.e. the composite PIOA). The method is based on symbolic calculations with vectors and matrices of rational functions, and it draws upon a theory of observables, which are mappings from delayed traces to real numbers that generalize the classical formal power series from algebra and combinatorics. Central to the theory is a notion of representation for an observable, which generalizes the classical notion linear representation for formal power series. As in the classical case, the representable observables coincide with an abstractly defined class of rational observables; this fact forms the foundation of our method.