Learning to Count up to Symmetry

TL;DR

This paper develops a theoretical framework for counting configurations in symmetric concurrent games, addressing the challenge of symmetry by identifying which configurations to count, and demonstrating preservation under composition.

Contribution

It introduces a novel counting theory for strategies in symmetric concurrent games, clarifying how to handle symmetry and invariance in counting configurations.

Findings

Counting is preserved under composition without deadlock.

Symmetry causes configurations to be considered equivalent, affecting counting.

Collapse operation to relational models is compatible with strategy composition.

Abstract

In this paper we develop the theory of how to count, in thin concurrent games, the configurations of a strategy witnessing that it reaches a certain configuration of the game. This plays a central role in many recent developments in concurrent games, whenever one aims to relate concurrent strategies with weighted relational models. The difficulty, of course, is symmetry: in the presence of symmetry many configurations of the strategy are, morally, different instances of the same, only differing on the inessential choice of copy indices. How do we know which ones to count? The purpose of the paper is to clarify that, uncovering many strange phenomena and fascinating pathological examples along the way. To illustrate the results, we show that a collapse operation to a simple weighted relational model simply counting witnesses is preserved under composition, provided the strategies involved do not deadlock.