Verification and Synthesis of Dynamic Network Algorithms

• Applicant: Professor Dr. Javier Esparza
• Subject Area: Theoretical Computer Science
• Term: since 2025
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 551606821

Classical models of distributed computation consist of relatively few computing agents with high computational resources, organized in a rigid communication structure (like an array, a ring, or a tree). In contrast, modern models have a very large number of components (even trillions in some natural computing models) with limited computational capabilities. They are organized in ad-hoc networks that may change dynamically. These emerging computational models, often called dynamic networks, have applications in areas like wireless networks, social networks, nanotechnology, natural computing, biology, and even physics. Population protocols are the most successful model in the theory of dynamic networks. A population protocol determines the behavior of a “soup” of indistinguishable mobile finite-state agents that randomly interact in pairs to decide whether their initial configuration satisfies a given property. In the last years we have developed the first software tools for automatically verifying correctness and time-complexity of a protocol. We have also designed synthesis procedures that, given a decision problem, automatically output a correct protocol for it. The population protocol model is being extended in different directions, mostly because of its applications to molecular programming. These extensions are revolutionizing the field. In particular, they have led to extremely fast algorithms for fundamental problems, like leader election and decentralized majority voting with indistinguishable voters, and to impressive implementations of algorithms executed by chemical or biological agents. The goal of this project is to develop the formal verification and synthesis theory for these extensions, and in particular for chemical reaction networks, a model of chemistry at the level of discrete molecules. It will focus on three questions: (1) Expressive power. Which decision problems can be solved by extensions of the population protocol model? (2) Verification. Which verification problems about the extensions are algorithmically decidable, and which is their complexity? How can one overcome undecidability or high-complexity barriers in practice? (3) Synthesis. Are there synthesis procedures that, given any decision problem, automatically produce a correct-by-construction protocol that solves it with a given amount of computational resources? The answers to these questions will be applied to case studies in molecular programming, biology, and social networks.

• DFG Programme: Reinhart Koselleck Projects