Interaction models describe distributed systems as algebraic terms, with gates marking interaction points between local views. Composing local models into a coherent global one requires aligning these gates while respecting the algebraic laws of interaction operators. We specialize anti-unification (or generalization) via a special constant-preserving variant, which preserves designated constants while generalizing the remaining structure. We develop a dedicated rule-based procedure for computing these generalizations, prove its termination, soundness, and completeness, extend it modulo equational theories, and integrate it into a standard anti-unification framework. A prototype tool demonstrates the approach's ability to recompose global interactions from partial views.
翻译:交互模型将分布式系统描述为代数项,其中门(gates)标记局部视图之间的交互点。将局部模型组合成一致的全局模型需要在遵循交互算子代数定律的同时对齐这些门。我们通过一种特殊的常量保持变体来实现专用反统一化(或称泛化),该方法在泛化剩余结构的同时保留指定的常量。我们开发了一种基于规则的专用程序来计算这些泛化,证明了其终止性、可靠性和完备性,将其扩展至模等式理论,并集成到标准的反统一化框架中。原型工具展示了该方法从局部视图重构全局交互的能力。