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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]