Schema della sezione

      • Minimizza Espandi

        Lesson 8

        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 \).