On Behaviour Equivalence for Probabilistic I/O Automata and its Relationship to Probabilistic Bisimulation

Previous work of the author has developed probabilistic input/output automata (PIOA) as a formalism for modelling systems that exhibit concurrent and probabilistic behaviour. Central to that work was the notion of the "behaviour map" associated with a state of a PIOA. The present paper presents a new, simpler definition for PIOA behaviour maps, investigates the induced "same behaviour 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 behaviour 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.