Advanced Topics in Bisimulation and Coinduction

Davide Sangiorgi and Jan Rutten, editors

Contents 
Preface 6 
Contributing authors 9 

1 Origins of Bisimulation and Coinduction 11
    Davide Sangiorgi 
1.1  Introduction  11 
1.2  Bisimulation in Modal Logic 13 
1.3  Bisimulation in Computer Science 17 
1.4  Set Theory 25 
1.5  The introduction of fixed points in Computer Science  36 
1.6  Fixed-point theorems 39
     Bibliography 41 

2 An introduction to (co)algebra and (co)induction  48
    Bart Jacobs and Jan Rutten 
2.1  Introduction 48 
2.2  Algebraic and coalgebraic phenomena 52 
2.3  Inductive and coinductive definitions 57 
2.4  Functoriality of products, coproducts and powersets 60 
2.5  Algebras and induction 63 
2.6  Coalgebras and coinduction 76 
2.7  Proofs by coinduction and bisimulation 85 
2.8  Processes coalgebraically 88 
2.9  Trace Semantics, coalgebraically 96 
2.10 Exercises 100
     Bibliography 104

3 The Algorithmics of Bisimilarity 109
    Luca Aceto, Anna Ingolfsdottir, and Jiri Srba 
3.1  Introduction 109 
3.2  Classic algorithms for bisimilarity 112 
3.3  The complexity of checking bisimilarity over finite processes 130 
3.4  Decidability results for bisimilarity 
     over infinite-state systems 151 
3.5  The use of bisimilarity checking in verification and tools 166
     Bibliography 173 

4 Bisimulation and Logic  182
    Colin Stirling 
4.1  Introduction 182 
4.2  Modal logic and bisimilarity 184 
4.3  Bisimulation invariance 188 
4.4  Modal mu-calculus 193 
4.5  Monadic second-order logic and bisimulation invariance 199
     Bibliography 205 

5 Howe's Method for Higher-Order Languages 206
    Andrew Pitts 
5.1  Introduction 206 
5.2  Call-by-value lambda-calculus  209 
5.3  Applicative (bi)similarity for call-by-value lambda-calculus 210 
5.4  Congruence 213 
5.5  Howe's construction 216 
5.6  Contextual equivalence 219 
5.7  The transitive closure trick 223 
5.8  CIU-equivalence 227 
5.9  Call-by-name equivalences 234 
5.10 Summary 238 
5.11 Assessment 239
     Bibliography 240 

6 Enhancements of the bisimulation proof method 243
    Damien Pous and Davide Sangiorgi 
6.1  The need for enhancements 245 
6.2  Examples of enhancements 249 
6.3  A theory of enhancements 259 
6.4  Congruence and up to context techniques 270
6.5  The case of weak bisimilarity 279 
6.6  A summary of up to techniques for bisimulation 295
     Bibliography 298 

7 Probabilistic bisimulation 300
    Prakash Panangaden 
7.1  Introduction 300
7.2  Discrete systems 305 
7.3  A Rapid Survey of Measure Theory 310 
7.4  Labelled Markov Processes 316 
7.5  Giry's monad 318 
7.6  Probabilistic Bisimulation 320 
7.7  Logical Characterization 322 
7.8  Probabilistic cocongruences 326 
7.9  Kozen's coinduction principle 330 
7.10 Conclusions 331
     Bibliography 334