Pith. sign in

REVIEW 5 major objections 6 minor 44 references

The paper claims that four message verbs plus typed options can encode every finite-state FIPA agent protocol and still support consensus-based coordination on severely resource-constrained devices.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-03 13:06 UTC pith:VIAO2PK4

load-bearing objection The paper's central claim—four verbs are complete—is close to vacuous because the encoding ships the original FIPA performative inside TLV options, and the proof rests on an unproved 'crucial observation'. the 5 major comments →

arxiv 2601.00219 v2 pith:VIAO2PK4 submitted 2026-01-01 cs.MA cs.NI

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

Arnab Mallick , Indraveni Chebolu This is my paper
classification cs.MA cs.NI
keywords agent communication languagemulti-agent systemsresource-constrained computingspeech act theorysemantic compressionconsensusprocess calculusFIPA-ACL
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper tries to establish that rich agent communication can be made cheap enough for microcontrollers. It defines a calculus named μACP built around just four message verbs — PING, TELL, ASK, OBSERVE — plus typed metadata options, and proves that every finite-state FIPA-style conversation with bounded nesting depth can be translated into μACP without changing observable behavior. The paper further claims near-optimal compression: encoded messages stay within a small constant of the Shannon entropy lower bound. It also shows that the same four verbs can implement standard consensus under partial synchrony and crash failures, meaning coordination with safety and liveness guarantees is achievable on constrained hardware. If correct, this reconciles a long-standing trade-off between semantic expressiveness and resource efficiency in multi-agent systems.

Core claim

On its own terms, μACP's central discovery is that a minimal four-verb basis {PING, TELL, ASK, OBSERVE}, combined with TLV options and correlation IDs, is semantically complete for finite-state FIPA-ACL performatives: for every performative there is a μACP message sequence whose observable trace matches the FIPA trace up to projection (Theorem 15). The compression theorem (Theorem 16) shows the encoding is within H + header + log k_max + 3 bits of the source entropy, i.e., near-optimal. The coordination theorem (Theorem 17) constructs a Paxos-style consensus implementation over these primitives, so any consensus-reducible coordination task inherits safety always and liveness after GST under

What carries the argument

The mechanism is the μACP message structure: a 64-bit header, a 2-bit verb field restricted to {PING, TELL, ASK, OBSERVE}, a bounded sequence of TLV (type-length-value) options for encoding conversational context like correlation IDs, ballots, and error flags, and a payload. This structure is tied to a labeled transition system with resource counters, and the completeness argument is carried by a simulation relation R between FIPA configurations and μACP configurations, built from matching belief atoms, conversation ids, and mirrored pending messages.

Load-bearing premise

The load-bearing premise is that every semantic effect of every FIPA performative can be realized by a finite sequence of the four verbs plus TLV option processing that updates an agent's local state; this 'crucial observation' is asserted in the proof sketch, not derived from a formal semantics of FIPA or of the TLV option processing.

What would settle it

A single counterexample would settle it: exhibit a finite-state, bounded-depth FIPA performative whose effect includes a refusal branch, a joint commitment, or some mental-state change that cannot be expressed as adding a finite set of ground literals to the recipient's knowledge base through TLV-triggered updates. Concretely, formalize the FIPA semantics for REQUEST with a REFUSE branch and the paper's ASK+TELL translation in a proof assistant, and check whether the refused run is trace-equivalent; if it is not, the completeness theorem collapses.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • FIPA-style conversations with finite state and bounded nesting depth can be run with a four-verb vocabulary, so the semantic overhead of traditional ACLs is not inherent.
  • No encoding of this message space can beat the entropy lower bound, and μACP is within a small additive constant, so further compression gains would be marginal.
  • Resource-constrained agents can run consensus-reducible coordination protocols with safety and liveness guarantees under crash faults, because the four-verb basis implements the needed message types.
  • Any finite execution satisfying feasibility keeps resource counters non-negative, so resource safety is guaranteed constructively.
  • The state space of the encodings grows exponentially with agent count with a small base, so verification remains tractable at practical scales.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the four-verb reduction holds, the same design principle—a minimal verb set plus typed metadata—should apply to other performative-heavy agent protocols, including modern JSON-based interoperability standards; this is a testable generalisation the paper does not explore.
  • The consensus reduction suggests an empirical test the paper did not run: measure actual consensus runs under μACP to see whether the reported median latency holds for Paxos-style traffic, since the simulation used negotiation workloads rather than consensus message patterns.
  • Because the completeness proof depends on syntactic realizability of FIPA pre/post conditions, the theorem only covers FIPA semantics that are belief-state based; commitment-based social semantics would require a new argument and may break the four-verb claim.
  • The compression bound includes k_max, the number of TLV option types; measuring how many types the full FIPA inventory actually needs would pin down the real constant and test whether it stays small in practice.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

5 major / 6 minor

Summary. The paper introduces µACP, a communication calculus with four message verbs (PING, TELL, ASK, OBSERVE) and TLV options, and claims three main results: (i) every finite-state FIPA-ACL protocol with bounded nesting depth can be encoded in µACP (Theorems 8 and 15); (ii) the encoding is near-optimal in message length (Theorem 16); and (iii) µACP can implement consensus under partial synchrony and crash faults, yielding safety and liveness (Theorem 17). The paper also reports TLA+ model checking, Coq proofs, and simulations to support these claims.

Significance. If the completeness and consensus theorems were rigorously proved, the minimal-verb basis and resource bounds would offer a useful bridge between expressive agent communication languages and constrained embedded systems. The paper is explicit about limitations (bounded nesting, no Byzantine) and reports mechanized verification and an empirical evaluation, which are commendable strengths. However, the central formal claims are not established: the main completeness proof relies on an undefined TLV-option semantics, one of the supporting theorems is false as stated, and the consensus proof is a high-level reduction sketch. As it stands, the contribution is a plausible research program rather than a verified calculus.

major comments (5)
  1. [Sec. 6.1, Theorem 15] The proof hinges on the 'crucial observation' that every FIPA pre/post condition is syntactically realizable via finite µACP transitions plus TLV state updates, but this is asserted, not proved. The TLV option-processing semantics is never defined: Definition 14 only states that O is a finite sequence from a bounded set, with no specification of which options exist or which state updates they invoke. In the local-simulation case for INFORM, the proof says the TELL transition 'adds φ to r's beliefs,' yet the operational semantics (Inference 4.1/4.2) only updates history and resource counters, not knowledge bases. Because τ can place arbitrary FIPA performatives in TLV options (e.g., τ(NOT-UNDERSTOOD)=PING+option(ERR, orig=m)), the four verbs reduce to an envelope; the expressive work is done by an unspecified option vocabulary. Without a formal semantics for TLV state updates, the complet
  2. [Sec. 4.3, Theorem 10] The proof asserts that 'since each run of C visits at most k distinct states, the encoding requires no more than k messages.' This is incorrect for cyclic automata: a run of a finite automaton can visit a state many times, so the number of transition steps—and hence the number of messages—is unbounded even when |Q|=k. The bound holds only for acyclic automata (or as a bound on distinct states, not on messages). This error undermines the procedural-completeness claim as stated.
  3. [Sec. 6.2, Theorem 16] The claimed 'tight' compression bound is not established. The entropy decomposition H(D)=H(V)+H(O|V)+H(P|V,O) treats O as the full option sequence, so adding ⌈log2 k_max⌉ on top of H(O|V) double-counts the option-type information; if O is intended to exclude types, the decomposition is inconsistent. The proof also absorbs E[K]·(⌈log2 L_max⌉) into constants without defining a uniform bound for all messages, and the derivation drops the dependence on the number of options. As written, the result is a restatement of Shannon's source-coding bound with additive overheads, not a tight characterization of µACP's message complexity.
  4. [Sec. 6.3, Theorem 17] The consensus reduction is a sketch rather than a proof. The claim that 'PING + adaptive timeouts implement an eventually accurate suspicion mechanism' after GST is nonstandard; partial synchrony alone does not guarantee an eventually perfect failure detector without additional assumptions on timeout bounds and communication. The statement that µACP 'can ensure' bounded-delivery after GST is an assumption on the environment, not a consequence of the calculus. No formal argument is given that the TLV-based encoding preserves the ballot ordering and majority-intersection invariants required for Paxos safety. Consequently, the theorem's safety/liveness conclusions do not follow from the presented arguments.
  5. [Sec. 4.3 / 6.1] The abstract and Theorem 8 claim 'observationally equivalent' encodings, but Theorem 15 proves only one inclusion (T_FIPA(P) ⊆ proj T_µACP(τ(P))). No converse inclusion or bisimulation is shown, so the equivalence claim is stronger than what is actually proved.
minor comments (6)
  1. [Abstract] Typo: 'is suffices' should be 'suffices'.
  2. [Sec. 4.3, Example 6] The example repeats the semantics already given in Equations (5)–(8); consider removing the duplication.
  3. [Sec. 4.2, Inference 4.1/4.2] The 'inference rules' are informal: side conditions are stated in prose and the state update is not specified recursively. Formalize the rules or clearly label them as informal summaries.
  4. [Sec. 7] TLA+ model checking of 'eventual delivery under partial synchrony' is not finite-state in general; describe the abstraction used for TLC to verify this property.
  5. [Sec. 8, Table 4] The claim of 'competitive or superior' latency is overstated given that MQTT on LAN has median <2 ms whereas µACP is 34 ms; clarify the network and load conditions for the comparison.
  6. [Sec. 6.2] The bound is stated in terms of H_hdr, k_max, and L_max, which are protocol parameters rather than universal constants; this should be made explicit in the theorem statement.

Circularity Check

2 steps flagged

Four-verb completeness is definitional: TLV options carry the original FIPA performative, so e(f) contains f and the 'minimal verb set' theorem reduces to an encoding choice.

specific steps
  1. self definitional [Section 4.3, Definition 9 (Procedural Encoding) and Theorem 10]
    "Definition 9 (Procedural Encoding). For a performative f requiring delegation or meta-communication: τ(f,cid)=(v,(=PROC,f)·(=CID,cid)) where v∈{ask,tell} and cid is a correlation identifier."

    The translation literally stores the original FIPA performative f as a TLV option value. Therefore any performative is representable because e(f) contains f itself; the four verbs are merely an envelope and the option vocabulary does the semantic work. The claimed 'procedural completeness' is thus true by construction, not by any property of the PING/TELL/ASK/OBSERVE basis.

  2. self definitional [Section 6.1, Theorem 15 proof (Translation and 'crucial observation')]
    "τ(NOT-UNDERSTOOD(s,r,m))=PING(r,s); option(ERR,orig=m) ... The crucial observation is that every FIPA pre/post condition is syntactically realizable via finite sequences of µACP primitive transitions plus TLV state updates. This is a finite, constructive mapping."

    The example encodes the original performative and its content in the TLV option (orig=m), so the observed effect is reproduced by carrying the FIPA act as data. The 'crucial observation' simply asserts the theorem's conclusion: that arbitrary FIPA pre/post conditions are realizable by µACP primitives plus TLV state updates. Since the TLV option-processing semantics is never defined, the four-verb completeness claim reduces to 'every performative can be named in an option,' which is definitional rather than a substantive expressiveness result.

full rationale

The paper's central theoretical claim—Theorem 15 (and its sketch Theorem 8) that four verbs are complete for finite-state FIPA—is circular in the specific sense that the encoding function τ places the original FIPA performative into the unrestricted TLV option field: τ(NOT-UNDERSTOOD(s,r,m))=PING(r,s); option(ERR,orig=m), and Definition 9 sets τ(f,cid)=(v,(=PROC,f)·(=CID,cid)). Thus Effect(f)=Effect(e(f)) holds because e(f) contains f as option data, not because the four verbs have expressive power. The proof's 'crucial observation' is an assertion of the theorem, and the semantics of TLV option-triggered state updates is unspecified. This makes the minimal-verb-set contribution largely vacuous as proved. The compression bound (Theorem 16) is not circular: it is a straightforward application of Shannon's source coding theorem with additive header/option constants. The consensus reduction (Theorem 17) is also an ordinary reduction to standard Paxos results and is not circular. However, the completeness theorem is load-bearing for the paper's 'four verbs suffice' claim, so the overall circularity score is high. The empirical and mechanized-verification sections do not repair this, since they model the same encoding choices rather than independently validating the expressiveness claim.

Axiom & Free-Parameter Ledger

4 free parameters · 7 axioms · 0 invented entities

The central claims rest on domain assumptions about partial synchrony and crash faults, plus an unproved assertion that TLV option processing can realize arbitrary FIPA effects. The compression theorem's additive constants (header size, option-type count, option-length bound) are protocol parameters rather than derived quantities.

free parameters (4)
  • H_hdr (header size) = 64 bits
    Fixed header size used in Theorem 16's compression bound; chosen by protocol design, not derived.
  • k_max (max TLV option types)
    Appears in the compression bound as an additive log k_max term; assumed finite, value unspecified, and treated as a constant in the proof.
  • L_max (max TLV option value length)
    Absorbed as a constant in the options part of the compression proof; no numerical value is given.
  • lambda_max (max message rate)
    Corollary 1 assumes agents operate under message rate <= lambda_max to conclude linear resource bounds.
axioms (7)
  • domain assumption Partial synchrony: there is an unknown GST after which message delivery on stable channels is bounded by Delta (Assumption 1).
    Used in Theorem 17 to derive consensus liveness; this is an environmental assumption, not a consequence of the calculus.
  • domain assumption Channel model: fair loss, arbitrary duplication, no spurious creation, eventual timeliness after GST (Assumption 2).
    Defines the network assumptions under which the consensus reduction holds.
  • domain assumption Crash/omission failures only, f < n/2; Byzantine faults excluded (Assumption 3).
    Bound for consensus safety; the paper later reports Byzantine experiments without reconciling this exclusion.
  • domain assumption Protocols are finite-state with bounded nesting depth d (Definition 14).
    Required for the completeness theorems; the paper itself lists recursive and unbounded conversations as a limitation.
  • ad hoc to paper Every FIPA pre/post condition is syntactically realizable by finite sequences of muACP transitions plus TLV state updates (Theorem 15 proof).
    This is the load-bearing unproved assertion that makes four-verb completeness work; no formal FIPA semantics or option-processing semantics is given.
  • standard math Shannon source coding theorem and entropy lower bound (Section 6.2).
    Used to assert no coding can beat H(D) and to derive the compression upper bound.
  • standard math Paxos correctness under partial synchrony as in Dwork-Lynch-Stockmeyer and Lamport (Theorem 17 proof).
    The consensus result is obtained by reduction to these standard theorems; they are assumed rather than reproved.

pith-pipeline@v1.3.0-alltime-deepseek · 13528 in / 18143 out tokens · 183476 ms · 2026-08-03T13:06:54.153010+00:00 · methodology

0 comments
read the original 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.

Figures

Figures reproduced from arXiv: 2601.00219 by Arnab Mallick, Indraveni Chebolu.

Figure 1
Figure 1. Figure 1: TLC state-space scaling (𝑛 = 3 . . . 7), confirming finite-state tractability of 𝜇ACP encodings. Exploration of 𝑛 = 3 . . . 7 agents with loss/duplication covered 106–107 states, with no counterexamples. State counts matched the exponential fit 𝑆 (𝑛) ≈ 5.2 · 104 · 1.80𝑛 , consistent with Theorem 15. All runs completed in < 100s, with runtime growth approximated by 𝑇 (𝑛) ≈ 0.53 · 𝑛 2.68, confirming tractabi… view at source ↗
Figure 2
Figure 2. Figure 2: ECDF of Coq lemma verification times: 76% under 0.5s, none above 2s. 8 EMPIRICAL VALIDATION We evaluate 𝜇ACP through microbenchmarks, heterogeneous device tests, and large-scale system simulations to assess efficiency, scalability, and robustness. Microbenchmarks and Heterogeneous Tests. Encoding/decoding 5,000 messages averaged 11.0 bytes (empty) and 23.0 bytes (with TLVs); per-message encode/decode times… view at source ↗
Figure 3
Figure 3. Figure 3: Max queue depth and mean throughput vs. agent count. Stable up to [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Negotiation outcomes: accept (blue) and reject (red). Sustained concurrency and throughput. Protocol / System Median (ms) 95th (ms) Max (ms) 𝜇ACP 34.07 103.88 130.48 MQTT (LAN, no-load) <2 20 200 MQTT (WAN/high-load) 50 100 250+ FIPA-ACL/JADE (MAS) 100 250 800+ CoAP (multi-hop) 20 100 300+ [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Histogram of message latencies. Majority delivered within 34 ms; tails bounded. [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Dropped messages per tick. No deadlock; only transient losses. [PITH_FULL_IMAGE:figures/full_fig_p017_6.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

44 extracted references · 8 canonical work pages

  1. [1]

    Ala Al-Fuqaha, Mohsen Guizani, Mehdi Mohammadi, Mohammed Aledhari, and Munther Ayyash. 2015. A survey on communication protocols for the Internet of Things.IEEE Communications Surveys & Tutorials17, 3 (2015), 1448–1468

    2015

  2. [2]

    Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, Gianluca Torta, and Mirko Viroli. 2024. Programming Distributed Collective Processes in the eXchange Calculus.Journal of Systems and Software197 (2024), 112976. https://doi.org/10.1016/j.jss.2024.111976 Special issue on Collective and Adaptive Systems

    arXiv 2024

  3. [3]

    J. L. Austin. 1962.How to Do Things with Words. Clarendon Press, Oxford, United Kingdom

    1962

  4. [4]

    Andrew Banks and Rahul Gupta. 2014. MQTT Version 3.1.1. OASIS Standard. https://docs.oasis-open.org/mqtt/mqtt/v3.1.1/os/mqtt- v3.1.1-os.html OASIS Standard

    2014

  5. [5]

    Yehoshua Bar-Hillel. 1964. Formal semantics of natural languages.Encyclopaedia Britannica16 (1964), 393–400

    1964

  6. [6]

    Chiara Bodei, Pierpaolo Degano, Gian-Luigi Ferrari, and Letterio Galletta. 2017. Tracing where IoT data are collected and aggregated. Logical Methods in Computer ScienceVolume 13, Issue 3 (jul 2017). https://doi.org/10.23638/lmcs-13(3:5)2017

    work page doi:10.23638/lmcs-13(3:5)2017 2017

  7. [7]

    Flavio Bonomi, Rodolfo Milito, Preethi Natarajan, Jiang Zhu, and Sateesh Addepalli. 2014. Fog Computing: A Platform for Internet of Things and Analytics. InBig Data and Internet of Things: A Roadmap for Smart Environments, Nick Bessis and Calin Dobre (Eds.). Studies in Computational Intelligence, Vol. 546. Springer, Cham, Switzerland, 169–186. https://doi...

    work page doi:10.1007/978-3-319-05029-4_7 2014

  8. [8]

    Jia Chen, Xu Ran, Honghao Gao, Tom H Luan, and Fengyu Zhou. 2020. Edge computing for IoT: A survey.IEEE Internet of Things Journal8, 5 (2020), 3224–3243

    2020

  9. [9]

    Ningning Chen and Huibiao Zhu. 2024. A process calculus SMrCaIT for IoT.Journal of Software: Evolution and Process36, 5 (2024), e2595. https://doi.org/10.1002/smr.2595 arXiv:https://onlinelibrary.wiley.com/doi/pdf/10.1002/smr.2595

    work page doi:10.1002/smr.2595 2024

  10. [10]

    Edmund M Clarke and E Allen Emerson. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifica- tions.ACM Transactions on Programming Languages and Systems (TOPLAS)8, 2 (1986), 244–263

    1986

  11. [11]

    Philip R Cohen and Hector J Levesque. 1990. Intention is choice with commitment.Artificial Intelligence42, 2-3 (1990), 213–261

    1990

  12. [12]

    Cover and Joy A

    Thomas M. Cover and Joy A. Thomas. 2006.Elements of Information Theory(2nd ed.). Wiley-Interscience, Hoboken, NJ, USA

    2006

  13. [13]

    Lynch, and Larry Stockmeyer

    Cynthia Dwork, Nancy A. Lynch, and Larry Stockmeyer. 1988. Consensus in the presence of partial synchrony.Journal of the ACM (JACM)35, 2 (1988), 288–323. https://doi.org/10.1145/42282.42283

    arXiv 1988

  14. [14]

    Abul Ehtesham, Aditi Singh, Gaurav Kumar Gupta, and Saket Kumar. 2025. A survey of agent interoperability protocols: Model Context Protocol (MCP), Agent Communication Protocol (ACP), Agent-to-Agent Protocol (A2A), and Agent Network Protocol (ANP). arXiv:2505.02279 [cs.AI] https://arxiv.org/abs/2505.02279

    Pith/arXiv arXiv 2025

  15. [15]

    Mohamed Amine Ferrag, Norbert Tihanyi, and Merouane Debbah. 2025. From LLM Reasoning to Autonomous AI Agents: A Compre- hensive Review. arXiv:2504.19678 [cs.AI] https://arxiv.org/abs/2504.19678 17

    Pith/arXiv arXiv 2025

  16. [16]

    Tim Finin, Richard Fritzson, Don McKay, and Robin McEntire. 1994. KQML as an Agent Communication Language. InProceedings of the Third International Conference on Information and Knowledge Management (CIKM ’94). ACM, Gaithersburg, Maryland, USA, 456–463. https://doi.org/10.1145/191246.191322

    arXiv 1994

  17. [17]

    1997.FIPA ACL Message Structure Specification

    FIPA. 1997.FIPA ACL Message Structure Specification. Technical Report. Foundation for Intelligent Physical Agents

    1997

  18. [18]

    Jayavardhana Gubbi, Rajkumar Buyya, Slaven Marusic, and Marimuthu Palaniswami. 2013. Internet of Things (IoT): A vision, architectural elements, and future directions.Future generation computer systems29, 7 (2013), 1645–1660

    2013

  19. [19]

    C. A. R. Hoare. 1985.Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs, NJ, USA

    1985

  20. [20]

    Holzmann

    Gerard J. Holzmann. 1991.Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, NJ, USA

    1991

  21. [21]

    Panagiotis Kouvaros, Elena Botoeva, and Cosmo De Bonis-Campbell. 2024. Formal Verification of Parameterised Neural-symbolic Multi-agent Systems. InProceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24, Kate Larson (Ed.). International Joint Conferences on Artificial Intelligence Organization, Jeju, 103–110. ht...

    doi:10.24963/ijcai.2024/12 2024

  22. [22]

    Yannis Labrou and Tim Finin. 1998. Semantics for an agent communication language. InIntelligent Agents IV Agent Theories, Architectures, and Languages, Munindar P. Singh, Anand Rao, and Michael J. Wooldridge (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 209–214

    1998

  23. [23]

    Leslie Lamport. 1994. The temporal logic of actions.ACM Trans. Program. Lang. Syst.16, 3 (May 1994), 872–923. https://doi.org/10. 1145/177492.177726

    arXiv 1994

  24. [24]

    Leslie Lamport. 2001. Paxos Made Simple.ACM SIGACT News (Distributed Computing Column)32, 4 (Dec. 2001), 51–58. https: //lamport.azurewebsites.net/pubs/paxos-simple.pdf Whole Number 121

    2001

  25. [25]

    Luca Mottola and Gian Pietro Picco. 2011. Programming wireless sensor networks: Fundamental concepts and state of the art.ACM Computing Surveys (CSUR)43, 3 (2011), 1–51

    2011

  26. [26]

    Muldoon, G

    C. Muldoon, G. M. P. O’Hare, R. Collier, and M. J. O’Grady. 2006. Agent Factory Micro Edition: A Framework for Ambient Applications. InComputational Science – ICCS 2006, Vassil N. Alexandrov, Geert Dick van Albada, Peter M. A. Sloot, and Jack Dongarra (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 727–734

    2006

  27. [27]

    Michele Pasqua and Marino Miculan. 2023. AbU: A Calculus for Distributed Event-driven Programming with Attribute-based Interaction. Theoretical Computer Science958 (2023), 113841. https://doi.org/10.1016/j.tcs.2023.113841

    arXiv 2023

  28. [28]

    Amir Pnueli. 1986. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. Lecture Notes in Computer Science224 (1986), 510–584. https://doi.org/10.1007/BFb0027047

    work page doi:10.1007/bfb0027047 1986

  29. [29]

    Gregory J Pottie and William J Kaiser. 2000. Wireless integrated network sensors.Commun. ACM43, 5 (2000), 51–58

    2000

  30. [30]

    Rao and Michael P

    Anand S. Rao and Michael P. Georgeff. 1991. Modeling Rational Agents within a BDI-Architecture. InProceedings of the Second International Conference on Principles of Knowledge Representation and Reasoning (KR’91). Morgan Kaufmann, Cambridge, MA, USA, 473–484

    1991

  31. [31]

    Mahadev Satyanarayanan. 2017. The emergence of edge computing.Computer50, 1 (2017), 30–39

    2017

  32. [32]

    2018.Agent-Based Computing in the Internet of Things: A Survey

    Claudio Savaglio, Giancarlo Fortino, Maria Ganzha, Marcin Paprzycki, Costin Bădică, and Mirjana Ivanović. 2018.Agent-Based Computing in the Internet of Things: A Survey. Springer International Publishing, Cham, 307–320. https://doi.org/10.1007/978-3-319-66379-1_27

    work page doi:10.1007/978-3-319-66379-1_27 2018

  33. [33]

    John R. Searle. 1969.Speech Acts: An Essay in the Philosophy of Language. Cambridge University Press, Cambridge, UK

    1969

  34. [34]

    Claude E Shannon. 1948. A mathematical theory of communication.The Bell system technical journal27, 3 (1948), 379–423

    1948

  35. [35]

    2014.The Constrained Application Protocol (CoAP)

    Zach Shelby, Klaus Hartke, and Carsten Bormann. 2014.The Constrained Application Protocol (CoAP). RFC 7252. Internet Engineering Task Force (IETF). https://datatracker.ietf.org/doc/rfc7252/ Standards Track

    2014

  36. [36]

    Munindar P Singh. 1998. Agent communication languages: rethinking the principles.Computer31, 12 (1998), 40–47

    1998

  37. [37]

    Munindar P. Singh. 2000.A Social Semantics for Agent Communication Languages. Springer Berlin Heidelberg, Berlin, Heidelberg, 31–45. https://doi.org/10.1007/10722777_3

    work page doi:10.1007/10722777_3 2000

  38. [38]

    Junsup Song, Sunghyun Lee, Dimitris Karagiannis, and Moonkun Lee. 2024. Process Algebraic Approach for Probabilistic Verification of Safety and Security Requirements of Smart IoT Systems in Digital Twin.Sensors24, 3 (2024), 767. https://doi.org/10.3390/s24030767

    work page doi:10.3390/s24030767 2024

  39. [39]

    Brett Warneke, Matt Last, Brian Liebowitz, and Kristofer S. J. Pister. 2001. Smart Dust: Communicating with a Cubic-Millimeter Computer.Computer34, 1 (Jan. 2001), 44–51

    2001

  40. [40]

    1999.Multiagent systems: a modern approach to distributed artificial intelligence

    Gerhard Weiss (Ed.). 1999.Multiagent systems: a modern approach to distributed artificial intelligence. MIT Press, Cambridge, MA, USA

    1999

  41. [41]

    2009.An Introduction to MultiAgent Systems(2nd ed.)

    Michael Wooldridge. 2009.An Introduction to MultiAgent Systems(2nd ed.). Wiley, Chichester, UK

    2009

  42. [42]

    Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Hao Wu, Bohua Zhan, Xinxin Liu, and Naijun Zhan. 2025. HpC: A Calculus for Hybrid and Mobile Systems.Proc. ACM Program. Lang.9, OOPSLA1, Article 121 (April 2025), 26 pages. https://doi.org/10.1145/3720478

    work page doi:10.1145/3720478 2025

  43. [43]

    Qingchen Zhang, Lin Yang, and Zhongyu Chen. 2021. Edge intelligence: The confluence of edge computing and artificial intelligence. IEEE Internet of Things Journal8, 14 (2021), 11025–11041

    2021

  44. [44]

    Jacob Ziv and Abraham Lempel. 1977. A universal algorithm for sequential data compression.IEEE Transactions on information theory 23, 3 (1977), 337–343. 18

    1977