Specializing anti-unification for interaction models composition via gate connections

TL;DR

This paper introduces a specialized anti-unification method for composing interaction models in distributed systems, ensuring consistent alignment of interaction points while preserving key constants, supported by a formal procedure and a prototype tool.

Contribution

It develops a constant-preserving anti-unification technique tailored for interaction model composition, with formal guarantees and integration into existing frameworks.

Findings

The specialized anti-unification preserves designated constants during generalization.

The rule-based procedure is proven to terminate, sound, and complete.

A prototype demonstrates effective recomposition of global interactions from partial views.

Abstract

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.