Coinduction is a method for specifying and reasoning about infinite data types and automata with infinite behaviour. In recent years, it has come to play an ever more important role in the theory of computing. It is studied in many disciplines, including process theory and concurrency, modal logic and automata theory. Typically, coinductive proofs demonstrate the equivalence of two objects by constructing a suitable bisimulation relation between them. This collection of surveys is aimed at both researchers and Master's students in computer science and mathematics and deals with various aspects of bisimulation and coinduction, with an emphasis on process theory. Seven chapters cover the following topics: history, algebra and coalgebra, algorithmics, logic, higher-order languages, enhancements of the bisimulation proof method, and probabilities. Exercises are also included to help the reader master new material.
Contents: 1. Origins of bisimulation and coinduction (Davide Sangiorgi) — 2. An introduction to (co)algebra and (co)induction (Bart Jacobs and Jan Rutten) — 3. The algorithmics of bisimilarity (Luca Aceto, Anna Ingolfsdottir and Jiří Srba) — 4. Bisimulation and logic (Colin Stirling) — 5. Howe’s method for higher-order languages (Andrew Pitts) — 6. Enhancements of the bisimulation proof method (Damien Pous and Davide Sangiorgi) — 7. Probabilistic bisimulation (Prakash Panangaden)
Author(s): Davide Sangiorgi, Jan Rutten (Editors)
Series: Cambridge Tracts in Theoretical Computer Science, Vol. 52
Publisher: Cambridge University Press
Year: 2012
Language: English
Pages: 342
Cover......Page 1
Abstract......Page 3
Title Page......Page 5
Contents......Page 7
Contributors......Page 10
Preface......Page 13
1.1 Introduction......Page 17
1.2.2 From homomorphism to p-morphism......Page 19
1.2.3 Johan van Benthem......Page 21
1.3.1 Algebraic theory of automata......Page 23
1.3.2 Robin Milner......Page 27
1.3.3 David Park......Page 29
1.3.4 Discussion......Page 30
1.4 Set theory......Page 31
1.4.1 Non-well-founded sets......Page 32
1.4.2 The stratified approach to set theory......Page 33
1.4.3 Non-well-founded sets and extensionality......Page 34
1.4.4 Marco Forti and Furio Honsell......Page 35
1.4.5 Peter Aczel......Page 36
1.4.7 Extensionality quotients: Roland Hinnion and others......Page 39
1.4.8 Discussion......Page 40
1.5 The introduction of fixed points in computer science......Page 42
1.6 Fixed-point theorems......Page 45
Bibliography......Page 47
2.1 Introduction......Page 54
2.2 Algebraic and coalgebraic phenomena......Page 58
2.3 Inductive and coinductive definitions......Page 63
2.4 Functoriality of products, coproducts and powersets......Page 66
2.5 Algebras and induction......Page 69
2.6 Coalgebras and coinduction......Page 82
2.7 Proofs by coinduction and bisimulation......Page 92
2.8 Processes coalgebraically......Page 95
2.9 Trace semantics, coalgebraically......Page 103
2.10 Exercises......Page 106
Bibliography......Page 110
3.1 Introduction......Page 116
3.2 Classical algorithms for bisimilarity......Page 118
3.2.1 Preliminaries......Page 120
3.2.2 The algorithm of Kanellakis and Smolka......Page 121
3.2.3 The algorithm of Paige and Tarjan......Page 126
3.2.4 Computing bisimilarity, symbolically......Page 132
3.2.5 Checking weak equivalences......Page 137
3.3.1 Game characterisation of bisimulation-like relations......Page 138
3.3.2 Deciding bisimilarity over finite labelled transition systems is P-complete......Page 139
3.3.3 EXPTIME-completeness of equivalence checking on networks of finite processes......Page 150
3.4.1 Process rewrite systems......Page 158
3.4.2 Deciding bisimilarity on BPP using a tableau technique......Page 163
3.4.3 Undecidability of bisimilarity on Petri nets......Page 169
3.4.4 Overview of results......Page 172
3.5 The use of bisimilarity checking in verification and tools......Page 173
3.5.1 Some uses of bisimilarity checking......Page 174
Bibliography......Page 179
4.1 Introduction......Page 189
4.2 Modal logic and bisimilarity......Page 191
4.3 Bisimulation invariance......Page 195
4.4 Modal mu-calculus......Page 200
4.5 Monadic second-order logic and bisimulation invariance......Page 206
Bibliography......Page 211
5.1 Introduction......Page 213
5.2 Call-by-value λ-calculus......Page 216
5.3 Applicative (bi)similarity for call-by-value λ-calculus......Page 217
5.4 Congruence......Page 220
5.5 Howe’s construction......Page 223
5.6 Contextual equivalence......Page 226
5.7 The transitive closure trick......Page 230
5.8 CIU-equivalence......Page 234
5.9 Call-by-name equivalences......Page 241
5.11 Assessment......Page 245
Bibliography......Page 246
6 Enhancements of the bisimulation proof method......Page 249
6.1.1 The bisimulation game......Page 251
6.1.2 Tracking redundancies......Page 252
6.2 Examples of enhancements......Page 255
6.2.1 Diagram-based enhancements......Page 256
6.2.2 Context-based enhancements......Page 258
6.2.3 Combining enhancements......Page 259
6.2.4.1 Unique solutions of equations......Page 260
6.2.4.2 Replication laws......Page 261
6.2.5 What is a redundant pair?......Page 263
6.3.1 Bisimulations and bisimilarity as coinductive objects......Page 265
6.3.2 Enhancements as functions......Page 268
6.3.3 Compositionality problems......Page 269
6.3.4.1 Symmetric functions......Page 273
6.3.4.2 Symmetric up-to techniques......Page 274
6.3.4.3 Non-symmetric up-to techniques......Page 275
6.4 Congruence and up to context techniques......Page 276
6.4.2 Up to context techniques......Page 277
6.4.3 Substitutivity......Page 278
6.4.5 An alternative method: initial contexts......Page 279
6.5 The case of weak bisimilarity......Page 285
6.5.2 Diagram-based techniques......Page 286
6.5.2.1 The problem with weak bisimilarity......Page 287
6.5.2.2 Up to strong bisimilarity......Page 288
6.5.2.3 The expansion preorder......Page 290
6.5.2.4 Non-symmetric up-to techniques......Page 291
6.5.2.5 Distinguishing between silent and visible transitions......Page 292
6.5.2.6 Beyond expansion: termination hypotheses......Page 294
6.5.3.1 The case of sum-free CCS......Page 297
6.5.4 Combining contexts and transitivity......Page 300
6.6.2 Weak bisimilarity......Page 302
Bibliography......Page 303
7.1 Introduction......Page 306
7.2 Discrete systems......Page 311
7.3 A rapid survey of measure theory......Page 316
7.4.1 Some examples......Page 322
7.4.2 Formal definitions......Page 323
7.5 Giry’s monad......Page 324
7.6.1 Categorical definition......Page 326
7.6.2 Relational definition......Page 328
7.7 Logical characterisation......Page 329
7.8 Probabilistic cocongruences......Page 332
7.9 Kozen’s coinduction principle......Page 335
7.10 Conclusions......Page 337
Bibliography......Page 339
