Institute of

Theoretical Computer Science


Technische Universität Braunschweig



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:


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



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


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