[Prev][Next][Index][Thread]

Book Announcement: "Logic for Concurrency and Synchronisation"

[please post]

Book Announcement

  Logic for Concurrency and Synchronisation
  Ruy J.G.B. de Queiroz (editor)
  Volume 18 of Trends in Logic
  Kluwer Academic Publishers, Dordrecht
  Hardbound, ISBN 1-4020-1270-5, xxi+284pp
  July 2003
  http://www.wkap.nl/prod/b/1-4020-1270-5

Foreword
by Johan van Benthem

The study of information-based actions and processes has been a vibrant
interface between logic and computer science for several decades now.
Indeed, several natural perspectives come together here. On the one hand,
logical systems may be used to describe the dynamics of arbitrary
computational processes - as in the many sophisticated process logics
available today. But also, key logical notions such as model checking or
proof search are themselves informational processes involving agents with
goals. The interplay between these descriptive and dynamic aspects shows
even in our ordinary language. A word like "proof" denotes both a static
'certificate' of truth, and an activity which humans or machines engage in.
Increasing our understanding of logics of this sort tells us something about
computer science, and about cognitive actions in general.

The individual chapters of this book show the state of the art in current
investigations of process calculi such as linear logic, pi-calculus,
and mu-calculus - with mainly two major paradigms at work, namely,
linear logic and modal logic. These techniques are applied to the title
themes of concurrency and synchronisation, but there are also many
repercussions for topics such as the geometry of proofs, categorial
semantics, and logics of graphs. Viewed together, the chapters also offer
exciting glimpses of future integration, as the reader moves back and forth
through the book. Obvious links include modal logics for proof graphs,
labeled deduction merging modal and linear logic, Chu spaces linking proof
theory and model theory, and bisimulation-style equivalences as a tool for
analyzing proof processes.

The combination of approaches and the pointers for further integration in
this book also suggests a grander vision for the field. In classical
computation theory, Church's Thesis provided a unification and driving
force. Likewise, modern process theory would benefit immensely from a
synthesis bringing together paradigms like modal logic, process algebra,
and linear logic - with their currently still separate worlds of
bisimulations, proofs, and normalisation. If this Grand Synthesis is ever
going to happen, books like this are needed!

                         Johan van Benthem, ILLC Amsterdam & CSLI Stanford


 Table of Contents

 List of Figures .........................................................   xi

 List of Tables ..........................................................   xv

 Foreword ................................................................ xvii
 Johan van Benthem

 Preface .................................................................  xix

 Contributing Authors ....................................................  xxi

 Part I:  From a Structural Perspective ..................................    1

 1 Geometry of Deduction via Graphs of Proofs ............................    3
   Anjolina Grisi de Oliveira and Ruy J. G. B. de Queiroz
   1 Motivation ..........................................................    4
   2 The idea of studying proofs as geometric objects ....................   12
   3 Proof-nets ..........................................................   17
   4 Logical flow graphs .................................................   34
   5 Multiple-conclusion classical calculi ...............................   50
   6 Finale ..............................................................   70

 2 Chu's Construction: A Proof-Theoretic Approach ........................   89
   Gianluigi Bellin
   1 Preface .............................................................   89
   2 The trip translation ................................................   93
   3 Chu's construction ..................................................   98
   4 Proof-nets, trips and translations ..................................  100

 3 Two Paradigms of Logical Computation in Affine Logic? .................  111
   Gianluigi Bellin
   1 Introduction ........................................................  112
   2 Sequent calculus of MAL + Mix .......................................  119
   3 Additive mix ........................................................  123
   4 Proof-nets for MAL + Mix ............................................  126
   5 Cut-elimination modulo irrelevance ..................................  138
   6 Symmetric reductions require Mix ....................................  141

 4 Proof Systems for pi-Calculus Logics ..................................  145
   Mads Dam
   1 Introduction ........................................................  146
   2 Preliminaries on the pi-calculus ....................................  148
   3 A pi-mu-calculus ....................................................  153
   4 Example specifications ..............................................  159
   5 Proof system, modal fragment ........................................  162
   6 Soundness and completeness for the modal fragment ...................  179
   7 Proof rules for recursive formulas ..................................  180
   8 Finite control completeness .........................................  188
   9 Natural numbers .....................................................  192
   10 Buffers ............................................................  194
   11 Conclusion .........................................................  196

 Part II: From a Descriptive Perspective .................................  213

 5 A Tutorial Introduction to Symbolic Model Checking ....................  215
   David Deharbe
   1 Introduction ........................................................  215
   2 Kripke structures ...................................................  216
   3 Temporal logic model checking .......................................  218
   4 Symbolic model checking .............................................  225
   5 Conclusion ..........................................................  233

 6 Modal Logics for Finite Graphs ........................................  239
   Mario R. F. Benevides
   1 Introduction ........................................................  239
   2 Finite directed graphs ..............................................  241
   3 Finite acyclic directed graphs ......................................  244
   4 Undirected graphs ...................................................  257
   5 Loopless undirected graphs ..........................................  257
   6 Modal definability ..................................................  258
   7 k-Colourable graphs .................................................  261
   8 Conclusions .........................................................  266

 7 Bisimulation and Language Equivalence .................................  269
   Colin Stirling
   1 Introduction ........................................................  269
   2 Background ..........................................................  270
   3 Caucal's hierarchy ..................................................  274
   4 Richer logics .......................................................  276
   5 Finite model theory .................................................  278

-------------------------------------------------------------------------------