Symmetric Synthesis

TL;DR

This paper investigates the complexity of synthesizing symmetric systems from specifications, showing EXPTIME-completeness for rotation-symmetric architectures and undecidability when processes lack full input access.

Contribution

It establishes the computational boundaries of symmetric synthesis, highlighting decidability in rotation-symmetric architectures and undecidability in more restricted models.

Findings

Symmetric synthesis is EXPTIME-complete for rotation-symmetric architectures.

The problem becomes undecidable when processes do not have full input access.

Symmetry simplifies system design and maintenance in distributed systems.

Abstract

We study the problem of determining whether a given temporal specification can be implemented by a symmetric system, i.e., a system composed from identical components. Symmetry is an important goal in the design of distributed systems, because systems that are composed from identical components are easier to build and maintain. We show that for the class of rotation-symmetric architectures, i.e., multi-process architectures where all processes have access to all system inputs, but see different rotations of the inputs, the symmetric synthesis problem is EXPTIME-complete in the number of processes. In architectures where the processes do not have access to all input variables, the symmetric synthesis problem becomes undecidable, even in cases where the standard distributed synthesis problem is decidable.