Process Symmetry in Probabilistic Transducers

TL;DR

This paper investigates various notions of symmetry in probabilistic systems, providing methods to decide whether a system exhibits exact or approximate symmetry with respect to process identities, which aids in system analysis and design.

Contribution

It introduces multiple variants of symmetry in probabilistic transducers and develops decision procedures for each, enhancing understanding of system behavior and simplifying specifications.

Findings

Defined precise symmetry and approximate symmetry variants.

Developed decision algorithms for each symmetry type.

Provided insights into system behavior through symmetry analysis.

Abstract

Model checking is the process of deciding whether a system satisfies a given specification. Often, when the setting comprises multiple processes, the specifications are over sets of input and output signals that correspond to individual processes. Then, many of the properties one wishes to specify are symmetric with respect to the processes identities. In this work, we consider the problem of deciding whether the given system exhibits symmetry with respect to the processes' identities. When the system is symmetric, this gives insight into the behaviour of the system, as well as allows the designer to use only representative specifications, instead of iterating over all possible process identities. Specifically, we consider probabilistic systems, and we propose several variants of symmetry. We start with precise symmetry, in which, given a permutation $\pi$, the system maintains the exact distribution of permuted outputs, given a permuted inputs. We proceed to study approximate versions of symmetry, including symmetry induced by small $L_\infty$ norm, variants of Parikh-image based symmetry, and qualitative symmetry. For each type of symmetry, we consider the problem of deciding whether a given system exhibits this type of symmetry.