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. This is achieved via anti-unification techniques. 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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Specializing Anti-unification for Interaction Models Composition via Gate Connections

  • Joel Nguetoum,
  • Boutheina Bannour,
  • Pascale Le Gall,
  • Erwan Mahe

摘要

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. This is achieved via anti-unification techniques. 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.