BIB-VERSION:: CS-TR-v2.0
          ID:: SBCS//stark/delays.ps.Z
       ENTRY:: December 5, 1997
ORGANIZATION:: State University of New York at Stony Brook, Computer Science
       TITLE:: Compositional Analysis of Expected Delays for Probabilistic
		I/O Automata
        TYPE:: Preprint
      AUTHOR:: Stark, Eugene W., and Smolka, Scott A.
     CONTACT:: Eugene W. Stark, Department of Computer Science,
                   SUNY at Stony Brook, Stony Brook, NY 11794-4400
                   Tel: 516-632-8444 <stark@cs.sunysb.edu>
        DATE:: December, 1997
   RETRIEVAL:: HTTP from BSD7.CS.SUNYSB.EDU with the URL
		   http://bsd7.cs.sunysb.edu/~stark/REPORTS/delays.ps.gz

ABSTRACT::

In previous work, we defined a notion of *probabilistic I/O automata*
(PIOA), and we showed that certain functions, which we called
``probabilistic behavior maps,'' constitute a compositional semantics for
PIOAs that is fully abstract with respect to a notion of testing equivalence.
We also observed that information about *completion probability* and
*expected completion time* for a ``closed PIOA'' can be extracted
from its behavior map.

In the present paper, we greatly extend and refine our previous results,
thereby obtaining a practical method for computing completion probabilities
and expected completion times.  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.
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
``formal power series'' from algebra and combinatorics.
We define *rational observables* to be those satisfying certain conditions,
among which is the condition that a certain vector space of ``derivatives''
be finite-dimensional.
Central to the theory is a notion of *representation* for an observable,
which generalizes the notion ``linear representation'' for formal power series.
We prove that the representable observables coincide with the rational ones;
this generalizes to observables a result of Carlyle and Paz equating the
recognizable series with those whose ``syntactic right ideal'' has finite
codimension.
We also present a minimization algorithm for representations of observables
that generalizes a result of Schuetzenberger for formal power series.
The minimization algorithm is applied in our analysis method to limit
combinatorial explosion that would otherwise occur.