[TYPES/announce] two books on bisimulation and coinduction

Tue Jan 17 07:31:06 EST 2012

I am pleased to announce the books:

-------------------------------------------------------
    Introduction to Bisimulation and Coinduction
    Davide Sangiorgi
    Cambridge University Press,260pp,ISBN:9781107003637
-------------------------------------------------------
    Advanced Topics in Bisimulation and Coinduction
    Davide Sangiorgi and Jan Rutten (eds)
    Cambridge University Press,340pp,ISBN:9781107004979
-------------------------------------------------------

The first book is an introduction to bisimulation and coinduction and
a precursor to the companion book on more advanced topics.
Throughout the two volumes, a special emphasis is given bisimulation
and processes. This because bisimulation is by far the most studied
coinductive concept, and because bisimulation was discovered in
Concurrency Theory and processes remain the main application area.

Below are blurbs and  tables of contents. For more details,
including order information, see:

http://www.cs.unibo.it/~sangio/IntroBook.html
http://www.cs.unibo.it/~sangio/AdvancedBook.html

Best regards,
Davide

INTRODUCTION TO BISIMULATION AND COINDUCTION
=======================================================

BLURB (from the cover page)

Induction is a pervasive tool in computer science and mathematics for
defining objects and reasoning on them. Coinduction is the dual of
induction, and as such it brings in quite different tools. Today, it
is widely used in computer science, but also in other fields,
including artificial intelligence, cognitive science, mathematics,
modal logics, philosophy and physics. The best-known instance of
coinduction is bisimulation, mainly employed to define and prove
equalities among potentially infinite objects: processes, streams,
non-well-founded sets, and so on.

This book presents bisimulation and coinduction: the fundamental concepts
and techniques, and the duality with induction. Each chapter contains
exercises and selected solutions, enabling students to connect theory with
practice. A special emphasis is placed on bisimulation as a behavioural
equivalence for processes. Thus the book serves as an introduction to 
models
for expressing processes (such as process calculi) and to the associated
techniques of operational and algebraic analysis.

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

ADVANCED TOPICS IN BISIMULATION AND COINDUCTION
=========================================================

BLURB (from the cover page)

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

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