Bisimulation relations for weighted automata

AbstractBisimulation is a well known equivalence relation for discrete event systems and has been extended to probabilistic and stochastic systems. This paper introduces a general definition of bisimulation which can be applied to finite automata where weights and labels are assigned to transitions. It is shown that this general view contains several known bisimulations as special cases and defines naturally equivalences for different classes of models. Apart from the well known forward bisimulation, also backward bisimulation is introduced and it is shown that both types of bisimulation preserve different types of results. Furthermore it is shown that forward and backward bisimulation are congruences according to commonly known composition operations for automata