Article (pdf). Functional morphisms of probabilistic automata are bisimulations. simulation equivalence does not imply bisimulation arbitrary morphisms do not imply bisimulation