Logic for Concurrency and Synchronisation
Ruy J.G.B. de Queiroz (ed.)
Kluwer Academic Publishers
The papers reviewed for publication in the volume are
full versions of contributions to the workshops of the project
with the same title (http://www.cin.ufpe.br/~locus).
The LOCUS Project, funded by the Brazilian
National Research Council (CNPq) was
concerned with the recent state-of-the-art regarding logic, computation and concurrency theory, including modal logics and the relationship between
proof theory (à la Curry-Howard-like calculi) and concurrency
theory (à la pi-calculus, mu-calculus).
The contributions to the volume could be classified into two groups:
the ones with emphasis on proof-theoretic issues (which might be called
"structural" approaches), and the ones concerned with (Kripke-style) models
(in this case, one might call "descriptive" approaches).
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
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
Part I: From a Structural Perspective
1. Geometry of Deduction via Graphs of Proofs
by Anjolina G. de Oliveira and Ruy J.G.B. de Queiroz
2. Chu's construction: A proof-theoretic approach
by Gianluigi Bellin
3. Two paradigms of logical computation in Affine Logic?
by Gianluigi Bellin
4. Proof Systems for pi-Calculus Logics
by Mads Dam
Part II: From a Descriptive Perspective
5. A tutorial introduction to symbolic model checking
by David Déharbe
6. Modal Logics for Finite Graphs
by Mario Benevides
7. Bisimulation and Language Equivalence
by Colin Stirling
Last Updated May 17, 11:38am GMT-0300.