We first study labeled transition systems with explicit successful termination.
We establish the notions of strong, weak, and branching bisimulation in terms
of boolean matrix theory, introducing thus a novel and powerful algebraic
apparatus. Next we consider Markov reward chains which are standardly presented
in real matrix theory. By interpreting the obtained matrix conditions for
bisimulations in this setting, we automatically obtain the definitions of
strong, weak, and branching bisimulation for Markov reward chains. The obtained
strong and weak bisimulations are shown to coincide with some existing notions,
while the obtained branching bisimulation is new, but its usefulness is
questionable. |