## Equivalence of Labeled Markov Chains

*Laurent Doyen,
Thomas A. Henzinger
and Jean-Francois Raskin*

We consider the equivalence problem for labeled Markov chains (LMCs),
where each state is labeled with an observation. Two LMCs are
equivalent if every finite sequence of observations has the same
probability of occurrence in the two LMCs. We show that equivalence
can be decided in polynomial time, using a reduction to the
equivalence problem for probabilistic automata, which is known to be
solvable in polynomial time. We provide an alternative algorithm to
solve the equivalence problem, which is based on a new definition of
bisimulation for probabilistic automata. We also extend the technique
to decide the equivalence of weighted probabilistic automata.

Then, we consider the equivalence problem for labeled Markov decision
processes (LMDPs), which asks given two LMDPs whether for every
scheduler (i.e., way of resolving the nondeterministic decisions) for
each of the processes, there exists a scheduler for the other process
such that the resulting LMCs are equivalent. The decidability of this
problem remains open. We show that the schedulers can be restricted
to be observation-based, but may require infinite memory.

*International Journal of Foundations of Computer Science* 19:549-563,
2008.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2008 World Scientific.