# Control Synthesis for Permutation-Symmetric High-Dimensional Systems With Counting Constraints

## TL;DR

This paper introduces a method for synthesizing correct controllers for high-dimensional, symmetric systems with counting constraints by leveraging symmetry and aggregate abstractions, enabling scalability to tens of thousands of states.

## Contribution

It presents a novel approach combining aggregate abstraction and linear inequality formulation to handle large, symmetric systems with complex counting constraints.

## Key findings

- Successfully synthesizes controllers for systems with tens of thousands of states.
- Demonstrates scalability and correctness of the approach.
- Effectively manages symmetry to reduce computational complexity.

## Abstract

General purpose correct-by-construction synthesis methods are limited to systems with low dimensionality or simple specifications. In this work we consider highly symmetrical counting problems and exploit the symmetry to synthesize provably correct controllers for systems with tens of thousands of states. The key ingredients of the solution are an aggregate abstraction procedure for mildly heterogeneous systems and a formulation of counting constraints as linear inequalities.