Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Thirteenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1998)

Paper: Compositional Analysis of Expected Delays in Networks of Probabilistic I/O Automata (at LICS 1998)

Authors: Eugene W. Stark Scott A. Smolka

Abstract

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

BibTeX

  @InProceedings{StarkSmolka-CompositionalAnalys,
    author = 	 {Eugene W. Stark and Scott A. Smolka},
    title = 	 {Compositional Analysis of Expected Delays in Networks of Probabilistic I/O Automata},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {466--477},
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski