Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A classification of bisimilarities for general Markov decision processes

Martín Santiago Moroni, Pedro Sánchez Terraf

Abstract

We provide a fine classification of bisimilarities between states of possibly different labelled Markov processes (LMP). We show that a bisimilarity relation proposed by Panangaden that uses direct sums coincides with "event bisimilarity" from his joint work with Danos, Desharnais, and Laviolette. We also extend Giorgio Bacci's notions of bisimilarity between two different processes to the case of nondeterministic LMP and generalize the game characterization of state bisimilarity by Clerc et al. for the latter.

A classification of bisimilarities for general Markov decision processes

Abstract

We provide a fine classification of bisimilarities between states of possibly different labelled Markov processes (LMP). We show that a bisimilarity relation proposed by Panangaden that uses direct sums coincides with "event bisimilarity" from his joint work with Danos, Desharnais, and Laviolette. We also extend Giorgio Bacci's notions of bisimilarity between two different processes to the case of nondeterministic LMP and generalize the game characterization of state bisimilarity by Clerc et al. for the latter.
Paper Structure (13 sections, 57 theorems, 46 equations, 2 figures, 1 table)

This paper contains 13 sections, 57 theorems, 46 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Labelled Markov processes
  4. Internal bisimulations
  5. External bisimulation
  6. $\wedge$-bisimulations and coalgebraic bisimilarity
  7. $\vee$-bisimulations
  8. External bisimilarities based on sums
  9. Comparison of notions for LMP and related work
  10. Nondeterministic processes
  11. External bisimulations for NLMP
  12. Game characterization
  13. Conclusion

Key Result

Lemma 2.1

Let $(S,\Sigma)$ and $(S',\Sigma')$ be measurable spaces. If $R$ is a binary relation such that $R\subseteq \mathop{\mathrm{inl}}\nolimits(S)^2 \cup \mathop{\mathrm{inr}}\nolimits(S')^2$, then $(\Sigma\oplus \Sigma')(R)\rest S=\Sigma(R\rest S)$. ∎

Figures (2)

  • Figure 1: The LMP $\mathbb{U}$.
  • Figure 2: The projection $\pi$ is $(\mathbf{LMP}\to\mathbf{Meas})$-final.

Theorems & Definitions (128)

  • Lemma 2.1
  • Definition 3.1
  • Definition 3.2
  • Example 3.3
  • Definition 3.4
  • Definition 3.5
  • Proposition 3.6
  • Example 3.7: State bisimilarity in Example \ref{['exm:lmp-U']}
  • Lemma 3.8
  • proof
  • ...and 118 more