Schema della sezione

  • Properties of bisimilarity: exercises and compositionality [RSBook 3.3]

    Exercises:

    • Exercises 3.3 and 3.5 in [RSBook]
    • Exercise 3.15 in RSBook (Barrier)
    • Exercise (Up-to bisimulation): A bisimulation up-to bisimilarity is a relation \(\mathbf{R} \subseteq \mathit{Proc} \times \mathit{Proc}\) such that, whenever \(P \mathbf{R} Q\) it holds that
      • for all \(P \stackrel{\alpha}{\to} P'\) there exists \(Q \stackrel{\alpha}{\to} Q'\) with \(P' \sim P'' \mathbf{R} Q'' \sim Q'\)
      • for all \(Q \stackrel{\alpha}{\to} Q'\) there exists \(P \stackrel{\alpha}{\to} P'\) with \(P' \sim P'' \mathbf{R} Q'' \sim Q'\)

               Show that if \( \mathbf{R}\) is a bisimulation up-to bisimilarity then \(P \mathbf{R} Q \) implies \( P \sim Q \).