The notion of weighted bisimulation [1]} generalizes
the well known notion from ordinary transition systems [2]} to
finite-state weighted automata. We follow the definition in
[3]} which applies to infinite state spaces, but with
finite branching: for all \(x \in X, a \in A, t(x)(a)(y) \ne 0\)  for
only finitely many \(y\) . In the following we assume the finite branching condition for
weighted automata without stating it explicitly.
