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 clasical notion "linea...

• Type: Conference
• Year: 1998
• Where: LICS
• Authors: Eugene W. Stark, Scott A. Smolka
• Keywords: Automated Reasoning, Formal Power Series, Global State Space, LICS 1998, Probabilistic I/o Automata