Metrics for Labeled Markov Systems

Josee Desharnais, Vineet Gupta, Radha Jagadeesan, Prakash Panangaden

Abstract

Partial Labeled Markov Chains are simultaneously generalizations of process algebra and of traditional Markov chains. They provide a foundation for interacting discrete probabilistic systems, the interaction being synchronization on labels as in process algebra. Existing notions of process equivalence are too sensitive to the exact probabilities of various transitions. This paper addresses contextual reasoning principles for reasoning about more robust notions of "approximate" equivalence between concurrent interacting probabilistic systems.

We develop a family of metrics between partial labeled Markov chains to formalize the notion of distance between processes.

We show that processes at distance zero are bisimilar.

We describe a decision procedure to compute the distance between two processes.

We show that reasoning about approximate equivalence can be done compositionally by showing that process combinators do not increase distance.

We introduce an asymptotic metric to capture asymptotic properties of Markov chains; and show that parallel composition does not increase asymptotic distance.

@InProceedings{metrics-concur99,
  author =       "Josee Desharnais and Vineet Gupta and Radha Jagadeesan and Prakash Panangaden",
  title =        "Metrics for Labeled Markov Processes",
  booktitle =    "Proceedings of CONCUR 99",
  editor=        "Jos Baeten and Sjouke Mauw",
  series =       "Lecture Notes in Computer Science",
  vol =          1664,
  publisher =    "Springer Verlag",
  year =         "1999",
  month =	 "August",
  pages =        "258-273"
}

Postscript file.