{\mu}ACP: A Formal Calculus for Expressive, Resource-Constrained Agent Communication

TL;DR

CP is a formal calculus designed for expressive, resource-constrained agent communication, balancing protocol expressiveness with efficiency through formal verification and practical performance evaluations.

Contribution

It introduces CP, a formal calculus that encodes standard protocols with minimal verbs, provides tight bounds on message complexity, and demonstrates practical efficiency and safety in resource-limited environments.

Findings

Minimal four-verb basis suffices for encoding FIPA protocols

Formal verification confirms safety and boundedness

Achieves median latency of 34 ms at scale

Abstract

Agent communication remains a foundational problem in multi-agent systems: protocols such as FIPA-ACL guarantee semantic richness but are intractable for constrained environments, while lightweight IoT protocols achieve efficiency at the expense of expressiveness. This paper presents $\mu$ACP, a formal calculus for expressive agent communication under explicit resource bounds. We formalize the Resource-Constrained Agent Communication (RCAC) model, prove that a minimal four-verb basis \textit{\{PING, TELL, ASK, OBSERVE\}} is suffices to encode finite-state FIPA protocols, and establish tight information-theoretic bounds on message complexity. We further show that $\mu$ACP can implement standard consensus under partial synchrony and crash faults, yielding a constructive coordination framework for edge-native agents. Formal verification in TLA$^{+}$ (model checking) and Coq (mechanized invariants) establishes safety and boundedness, and supports liveness under modeled assumptions. Large-scale system simulations confirm ACP achieves a median end-to-end message latency of 34 ms (95th percentile 104 ms) at scale, outperforming prior agent and IoT protocols under severe resource constraints. The main contribution is a unified calculus that reconciles semantic expressiveness with provable efficiency, providing a rigorous foundation for the next generation of resource-constrained multi-agent systems.