Equivalence of Labelled Markov Chains

Jean-François Raskin
Friday, 30 May, 2008 (All day)

We consider the equivalence problem for probabilistic machines. Two probabilistic machines are equivalent if every finite sequence of observations has the same probability of occurrence in the two machines. We show that deciding equivalence can be done in polynomial time for labeled Markov chains, 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 machines. We also extend that technique to decide 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 way of resolving the decisions in each of the processes, there exists a way of resolving the decisions in the other process such that the resulting probabilistic machines are equivalent. The decidability of this problem remains open. We show that the strategies used to resolve the decisions can be restricted to be observation-based, but may require infinite memory. Keywords: Labeled Markov chain, Markov decision process, probabilistic automaton, equivalence, bisimulation.

Joint work with Tom Henzinger and Laurent Doyen