Symmetry Preservation in Modular Rewritable Muliformalism Models

Arecent Maude formalization of multiformalism models for adaptive distributed systems makes it possible to build a symmetry-aware quotient transition system (TS) by means of compositional operators and a systematic node-labeling strategy that reflects the model’s hierarchical modular organization. In the stochastic setting, strong bisimilarity on the TS coincides with exact lumpability of the underlying Markov process. We address the challenge of preserving symmetry when Maude rewrite rules perform non-trivial transformations and, using a running example, derive conditions under which such transformations still preserve symmetry