BIB-VERSION:: CS-TR-v2.0
          ID:: SBCS//stark/pioalang.pdf
       ENTRY:: February 11, 2004
ORGANIZATION:: State University of New York at Stony Brook, Computer Science
       TITLE:: A Process-Algebraic Language for Probabilistic I/O Automata
        TYPE:: Technical Report
      AUTHOR:: Stark, E. W., Cleaveland, R., Smolka, S. A.
     CONTACT:: Eugene W. Stark, Department of Computer Science,
                   SUNY at Stony Brook, Stony Brook, NY 11794-4400
                   Tel: 631-632-8444 <stark@cs.sunysb.edu>
        DATE:: June 8, 2003
   RETRIEVAL:: HTTP from BSD7.CS.SUNYSB.EDU with the URL
		   http://bsd7.cs.sunysb.edu/~pioa/Papers/pioalang.abstract

ABSTRACT::

We present a process-algebraic language for Probabilistic I/O Automata
(PIOA).  To ensure that PIOA specifications given in our language
satisfy the ``input-enabled'' property, which requires that all input
actions be enabled in every state of a PIOA, we augment the language
with a set of *type inference rules*.  We also equip our language
with a formal operational semantics defined by a set of
*transition rules*.  We present a number of results whose thrust
is to establish that the typing and transition rules are sensible and
interact properly.  The central connection between types and
transition systems is that if a term is well-typed, then in fact the
associated transition system is input-enabled.  We also consider two
notions of equivalence for our language, *weighted bisimulation
equivalence* and *PIOA behavioral equivalence*.  We show that
both equivalences are substitutive with respect to the operators of
the language, and note that weighted bisimulation equivalence is a
strict refinement of behavioral equivalence.