An Introduction to Bisimulation and Coinduction

Davide Sangiorgi,  University of Bologna and INRIA

Contents

List of Illustrations ix 
List of Tables xi 

1 General introduction 1 
1.1 Why bisimulation and coinduction  1 
1.2 Objectives of the book 4 
1.3 Use of the book 5 
1.4 Structure of the book 6 
1.5 Basic definitions and mathematical notations 7

2 Towards bisimulation 11 
2.1 From functions to processes 11 
2.2 Interaction and behaviour 13 
2.3 Equality of behaviours 16 
2.4 Bisimulation 19

3 Coinduction and the duality with induction 28 
3.1 Examples of induction and coinduction 30 
3.2 The duality  37 
3.3 Fixed points in complete lattices 40 
3.4 Inductively and coinductively defined sets 45 
3.5 Definitions by means of rules 47 
3.6 The examples, continued 50 
3.7 Other induction and coinduction principles 57 
3.8 Constructive proofs of the existence 
    of least and greatest fixed points 66 
3.9 Continuity and cocontinuity, for rules 71
3.10 Bisimilarity as a fixed point 73 
3.11 Proofs of membership 79 
3.12 Game interpretations 83 
3.13 The bisimulation game 86 
3.14 A simpler bisimulation game 86

4 Algebraic properties of bisimilarity 89 
4.1 Basic process operators 90 
4.2 CCS 92 
4.3 Examples of equalities 94 
4.4 Some algebraic laws 96 
4.5 Compositionality properties 98 
4.6 Algebraic characterisation 103

5 Processes with Internal Activities 108 
5.1 Weak LTSs and weak transitions 109 
5.2 Weak bisimulation 110 
5.3 Divergence 115 
5.4 Rooted weak bisimilarity 118 
5.5 Axiomatisation 120 
5.6 On the bisimulation game for internal moves 123 
5.7 Bisimulation with divergence 124 
5.8 Dynamic bisimulation 126 
5.9 Branching bisimulation, eta-bisimulation, 
    and delay bisimulation 126

6 Other approaches to behavioural equivalences 133 
6.1 A testing scenario 135 
6.2 Bisimulation via testing 136 
6.3 Tests for weak bisimilarities 144 
6.4 Processes as testers 146 
6.5 Testing preorders 147 
6.6 Examples 149 
6.7 Characterisations of the may, must, 
    and testing relations 150 
6.8 Testing in weak LTSs 152 
6.9 Refusal equivalence 156 
6.10 Failure equivalence 157 
6.11 Ready equivalence 159 
6.12 Equivalences induced by SOS formats 160 
6.13 Non-interleaving equivalences 165 
6.14 Varieties in concurrency 165

7 Refinements of simulation  168 
7.1 Complete simulation 168 
7.2 Ready simulation 169 
7.3 2-nested simulation equivalence 171
7.4 Weak simulations 173
7.5 Coupled simulation 174
7.6 The equivalence spectrum 180

8 Basic observables  182
8.1 Labelled bisimilarities: examples of problems 184
8.2 Reduction congruence 185
8.3 Barbed congruence 188
8.4 Barbed equivalence 191
8.5 The weak barbed relations 192
8.6 Reduction-closed barbed congruence 194
8.7 Final remarks 196

Appendix 1 Solutions to selected exercises 199
List of Notations 231 
Bibliography 235 
Index 244