Proof systems for pi-calculus logics
Mads Dam · 2002
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 --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...