Institute of

Theoretical Computer Science

Carl-Friedrich-Gauß-Fakultät

Technische Universität Braunschweig

Pi-Calculus

Pi-Calculus

Concurrency is pervasive in computing. A standard approach is to organise concurrent software systems as a dynamic collection of processes that communicate by message passing. Because processes may be destroyed or created, the number of processes in the system changes in the course of the computation, and may be unbounded. Moreover the messages that are exchanged may contain process addresses. Consequently the communication topology of the system (the hypergraph connecting processes that can communicate directly) evolves over time. The design and analysis of these systems is difficult: the dynamic reconfigurability alone renders verification problems undecidable.

A popular model for these kind of systems is the pi-calculus. We study various restrictions on the behaviour of a system that enable the application of automatic verification techniques. The main fragment we study is the depth-bounded pi-calculus: a pi-term is depth-bounded if there is a number k such that every simple path in the communication topology of every reachable pi-term has length bounded by k.

We study some key problems related to depth boundedness and related fragments:

Team:

Roland Meyer, Emanuele D'Osualdo, and Reiner Hüchting

Publications:

Material:

Coverability tool for structural stationary systems Petruchio | A type system and playground for the depth-bounded pi-calculus James Bound

Funding:

DFG: Trustworthy Software Systems (GK TrustSoft) | DFG: Automatic Verification and Analysis of Complex Systems (SFB AVACS)