Theoretical Computer Science

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:

• How can depth-bounded systems be analysed?
• What is the complexity of verification tasks?
• How can we prove depth boundedness itself?
• How does depth boundedness relate to other fragments/models of computation?

Team:

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

Publications:

• On Hierarchical Communication Topologies in the pi-calculus, by Emanuele D'Osualdo and C.-H. Luke Ong.
  In Proceedings of ESOP 2016.
  DOI | arXiv | Tool

• Bounds on Mobility, by Reiner Hüchting, Rupak Majumdar, and Roland Meyer.
  In Proceedings of CONCUR 2014.
  PDF | DOI | BibTeX

• A Theory of Name Boundedness, by Reiner Hüchting, Rupak Majumdar, and Roland Meyer.
  In Proceedings of CONCUR 2013.
  PDF | DOI

• Provenance Verification, by Rupak Majumdar, Roland Meyer, and Zilong Wang.
  In Proceedings of RP 2013.
  DOI | BibTeX

• Static Provenance Verification for Message Passing Programs, by Rupak Majumdar, Roland Meyer, and Zilong Wang.
  In Proceedings of SAS 2013.
  PDF | DOI | BibTeX

• A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets, by Roland Meyer, Victor Khomenko, and Reiner Hüchting.
  In Proceedings of CONCUR 2012.
  PDF | DOI

• Petruchio: From dynamic networks to nets, by Roland Meyer and Tim Strazny.
  In Proceedings of CAV 2010.
  PDF | DOI | BibTeX

• On the relationship between pi-calculus and finite place/transition Petri nets, by Roland Meyer and Roberto Gorrieri.
  In Proceedings of CONCUR 2009.
  Slides | PDF | DOI | BibTeX

• Checking pi-calculus structural congruence is graph isomorphism complete, by Victor Khomenko and Roland Meyer.
  In Proceedings of ACSD 2009.
  DOI | PDF | BibTeX

• Strukturelle Stationarität, by Roland Meyer.
  In Ausgezeichnete Informatik Dissertationen, 2009.
  PDF, in German | BibTeX

• A practical approach to verification of mobile systems using net unfoldings, by Roland Meyer, Victor Khomenko, and Tim Strazny.
  In Proceedings of PETRI NETS 2008.
  Slides | PDF | DOI | BibTeX

• On boundedness in depth in the pi-calculus, by Roland Meyer.
  In Proceedings of IFIP TCS 2008.
  Slides | PDF | DOI | BibTeX

• A Polynomial Translation of Pi-Calculus (FCP) to Safe Petri Nets, by Victor Khomenko, Roland Meyer, and Reiner Hüchting.
  Logical Methods in Computer Science, 2013.
  arXiv | BibTeX

• A Theory of Structural Stationarity in the Pi-Calculus, by Roland Meyer.
  Acta Informatica, 2009.
  DOI | BibTeX

• A Practical Approach to Verification of Mobile Systems using Net Unfoldings, by Roland Meyer, Victor Khomenko, and Tim Strazny.
  Fundamenta Informaticae, 2009.
  DOI | BibTeX

• Structural Stationarity in the pi-Calculus, PhD thesis by Roland Meyer.
  Department of Computing Science, University of Oldenburg, 2009.
  Slides | PDF | BibTeX

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)