Research internship (Master M2) Title Synthesis of Distributed Systems with Parameterized Network Topology Description

We consider distributed programs that can be run on an arbitrary network topology from a class of topologies (e.g., on all pipeline, all grid, or all ring topologies). Typically, such a program is given by a single sequential process, and a copy of that process can be run on any node in the given network topology. During its execution, each process may receive signals from an (uncontrollable) environment. In parameterized synthesis, a specification ϕ is given (e.g., a temporal-logic formula) describ-ing the desired system behavior. The goal is then to synthesize a program that implements ϕ. Thus, the program acts as a collection of local controllers that enforce the system to satisfy ϕ, independently of the network topology and independently of the behavior of the environment. There have been, so far, only a few approaches to parameterized synthesis [1, 2]. Existing works consider specifications that are interpreted over sequentialized executions of a system. The aim of the internship is to develop a framework for parameterized synthesis in a setting with real concurrency, where the specification is interpreted over partially ordered behaviors reflecting the parallelism. This will combine [1, 2], [3], and [4], where parameterized synthesis, partial-orde