Paper: Proof systems for pi-calculus logics

["Mads Dam" <mfd@xxxxxxx>]

Dear all,

This is an announcement of a paper which summarizes some
work I've done over the last few years on building general-purpose
(i.e. not restricted to finite-control) mu-calculus based
proof systems for pi calculus. The paper is to appear
in R. de Queiroz (ed.), "Logic for Concurrency and 
Synchronisation",  a volume in the series Studies in Logic 
and Computation, Oxford  Univ Press.

Title: Proof Systems for pi-Calculus Logics

Author: Mads Dam

Abstract:
In this paper we study the problem of verifying general temporal
and functional properties of mobile and dynamic process networks,
cast in terms of the pi-calculus. Much of the expressive power of
this calculus derives from the combination of name generation and
communication (to handle mobility) with dynamic
process creation. In the paper we introduce the $\pi$-$\mu$-calculus, an
extension of the modal mu-calculus with name equality, inequality,
first-order universal and existential quantification, and
primitives for name input and output as an appropriate
temporal logic for the pi-calculus. A compositional proof
system is given with the scope of verifying dynamic networks
of pi-calculus agents against properties specified in this logic.
The proof system consists of a local part based, roughly, on
the classical sequent calculus extended with data structures for
private names, and rules to support process structure dependent
reasoning. In addition the proof system contains a rule of discharge
to close well-founded cycles in the proof graph.
The proof system is shown to be sound in general and weakly complete
for the non-recursive fragment of the specification logic.
We also obtain a weak completeness result for recursive formulas
against finite-control calculus processes.
Two examples are considered. The first example is based on
Milner's encoding of data types into the pi-calculus, specifically
the natural numbers. This encoding is interesting from the point of
view of verification, since it makes essential
use of all the distinguishing features of the pi-calculus, including
dynamic process creation. Corresponding to the encoding of
natural numbers into the $\pi$-calculus we propose an encoding
of the type of natural numbers into the $\pi$-$\mu$-calculus and
establish some type correctness properties. As the second example
we consider a garbage-collecting unbounded buffer (which
dynamically create and destroy buffer cells) and show how to
establish absence of spurious output of such a system.

The paper is available through
ftp://ftp.sics.se/pub/fdt/mfd/ProofSystemsPiCalLogics.ps.

Bests,

          Mads