BIB-VERSION:: CS-TR-v2.0
          ID:: SBCS//stark/bisimulation.ps.gz
       ENTRY:: January 3, 2003
ORGANIZATION:: State University of New York at Stony Brook, Computer Science
       TITLE:: Implementation of a Compositional Performance Analysis
			 Algorithm for Probabilistic I/O Automata
        TYPE:: Technical Report
      AUTHOR:: Stark, Eugene W.
     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:: January 3, 2003
   RETRIEVAL:: HTTP from BSD7.CS.SUNYSB.EDU with the URL
		   http://bsd7.cs.sunysb.edu/~pioa/Papers/bisimulation.abstract

ABSTRACT::

Previous work of the author has developed "probabilistic input/output
automata" (PIOA) as a formalism for modeling systems that exhibit
concurrent and probabilistic behavior.  Central to that work was the
notion of the "behavior map" associated with a state of a PIOA.  The
present paper presents a new, simpler definition for PIOA behavior
maps, investigates the induced "same behavior map" equivalence
relation, and compares it with the standard notion of probabilistic
bisimulation equivalence.  "Weighted finite automata" are used as a
unifying formalism to facilitate the comparison.  A general notion of
congruence for weighted automata is defined, which relates "signed
measures" on states, rather than just individual states.  PIOA are
defined as a class of weighted automata, as are the class of
"probabilistic weighted automata" for which the standard definition of
probabilistic bisimulation makes sense.  A characterization is
obtained of probabilistic bisimulation as the largest congruence that
is in a sense generated by its restriction to a relation on states.
This characterization is then used as the definition of "weighted
bisimulation", which generalizes probabilistic bisimulation to the
full class of weighted automata.  PIOA behavior equivalence is also
shown to define a weighted automata congruence, which is strictly
refined by weighted bisimulation equivalence.  The relationship
between these congruences and a notion of "composition" for weighted
automata is also examined.