pith. sign in

arxiv: 2407.06968 · v8 · pith:GWXO5LDEnew · submitted 2024-07-09 · 💻 cs.LO · cs.FL

An automata-based approach for synchronizable mailbox communication

Romain Delpy , Anca Muscholl , Gr\'egoire Sutre This is my paper

Pith reviewed 2026-05-23 23:20 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords communicating systemsmailbox semanticsround-based communicationsynchronizabilityPspace-completeautomata constructionsdistributed systemsFIFO buffers
0
0 comments X

The pith

Checking if a mailbox communication system complies with round-based policy without round size limits is Pspace-complete.

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

The paper shows that deciding whether every execution of a finite-state mailbox system can be re-scheduled into an equivalent sequence of rounds is Pspace-complete when rounds have unbounded size. It does so by constructing automata that model the mailbox semantics and the round-based restriction while preserving the property that executions remain equivalent after re-scheduling. This complexity result also pins down the exact complexity of several related questions previously studied under mailbox semantics. A sympathetic reader would care because the result supplies both a decision procedure and a tight complexity bound for verifying a natural communication discipline in distributed systems.

Core claim

The central claim is that the problem of determining whether a finite-state communicating system with one mailbox per process satisfies the round-based policy with no size limitation on rounds is Pspace-complete. The proof relies on a novel automata-based construction that encodes the mailbox semantics and the send-then-receive round discipline while preserving synchronizability, i.e., the existence of an equivalent round-respecting execution for every original execution.

What carries the argument

The automata constructions that encode mailbox semantics under the round-based policy while preserving the synchronizability property.

If this is right

  • Synchronizability of mailbox systems with unbounded rounds can be decided in polynomial space.
  • Several questions on mailbox communication studied in prior literature have Pspace complexity.
  • The automata constructions decide whether every execution admits an equivalent round-respecting re-scheduling.

Where Pith is reading between the lines

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

  • The same automata technique might be adapted to decide related properties such as absence of deadlocks under the same communication model.
  • If the construction works for unbounded rounds, it suggests the complexity does not jump when moving from fixed-size to variable-size rounds.
  • Similar automata encodings could be explored for peer-to-peer buffer models to compare their verification complexity.

Load-bearing premise

Finite-state communicating systems allow the mailbox semantics and round-based policy to be faithfully captured by automata constructions that preserve the synchronizability property.

What would settle it

An explicit finite-state mailbox system whose set of executions cannot be accepted by the constructed automata for the round-based policy, or whose synchronizability decision requires more than polynomial space, would falsify the Pspace-completeness claim.

Figures

Figures reproduced from arXiv: 2407.06968 by Anca Muscholl, Gr\'egoire Sutre, Romain Delpy.

Figure 1
Figure 1. Figure 1: A sequence and its MSC. An unmatched send action is marked by a special arrowhead, as for m2. Definition 2.9 (Message Sequence Chart). An MSC over P is an Act-labeled partially ordered set M = (E, ≤hb, λ) of events E, with λ : E → Act and ≤hb = (≤P ∪ msg) ∗ the least partial order containing the relations ≤P and msg, which are defined as: (1) For every process p, the set of events on p is totally ordered b… view at source ↗
Figure 2
Figure 2. Figure 2: The MSC of a trace of the CFM for automata intersection. For C we take the automaton Qsync constructed according to Lemma 3.4, and set the initial state to (g, D) and the final state to (g ′ , D′ ). For B, we need to tinker a bit with Qsync to ensure that we read only one exchange. So we remove all transitions from/to states in L × 2 P except the transitions from (g, D), which we set as initial, and the tr… view at source ↗
Figure 3
Figure 3. Figure 3: Gadget to reduce reachability in peer-to-peer semantics to non-mailbox￾similarity. p1 p2 p3 [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: MSC of u = p2!p1(m1) p1!p2(m2) p1?p2(m1) p2?p1(m2) p3!p2(m3), with the two SCCs of its communication graph. Note that 1 ⪯u mb 2, but neither 1 ⪯u p2p 2 nor 2 ⪯u p2p 1 holds. that Q is R-diamond, so Qr is R-closed. Let Pr denote the R-diamond automaton obtained from Lemma 4.6, and let Pr denote its R-closed language Pr = L(Pr). It is routinely checked that A is mailbox-similar iff for every r ∈ R, the set S… view at source ↗
Figure 6
Figure 6. Figure 6: A well-labeling of the ms-sequence bottom right, witnessing a path in the communication graph of the MSC left, from the last to the first event of process p1. The si and ri vertices of the communication graph correspond respectively to the send and receive of message mi . Proof. Let HN (u) be the N -communication graph of msc(u). By Lemma 5.3 the SCCs C1, . . . , Ck of HN (u) induce N -atomic subsequences … view at source ↗
Figure 7
Figure 7. Figure 7: The MSC of an atomic sequence. It is not mb-synchronizable by Lemma 5.13, each ui consists of message i, the indices are (1, 2, 3, 5), and m = 2. (4) There exists 1 ≤ m < k such that vim contains a receive by p and vim+1 a send by p. Proof. First the left-to-right direction. By assumption, u = v r with u not mb-synchronizable and v is mb-synchronizable. By Lemma 5.11 we can assume w.l.o.g. that v ≡ v1 ∗mb … view at source ↗
Figure 8
Figure 8. Figure 8: A weakly-synchronous sequence [BGF+21] that is not mb￾synchronizable. This way, the CFM is mb-synchronizable if and only if the intersection of the automata A1, . . . , An is empty. Theorem 5.16 yields two interesting corollaries. We define a k-mb-exchange as any mb￾viable sequence in S ≤kR∗ . An mb-viable sequence is k-mb-synchronous if it is a ∗mb-product of k-mb-exchanges, and is called k-mb-synchroniza… view at source ↗
Figure 10
Figure 10. Figure 10: A mb-send￾synchronizable CFM that is not 1-mb-synchronizable 7. Conclusion We have introduced a novel automata-based approach to reason about communication in the sr-round mailbox model. We showed that knowing whether a system complies with this model is Pspace-complete. An interesting theoretical question is whether we can apply similar techniques to other types of communication. On the practical side it… view at source ↗
read the original abstract

We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. Previous work mostly considered the setting where rounds have fixed size. Our main contribution shows that the problem whether a mailbox communication system complies with the round-based policy, with no size limitation on rounds, is Pspace-complete. For this we use a novel automata-based approach, that also allows to determine the precise complexity (Pspace) of several questions considered in previous literature.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper revisits finite-state communicating systems under mailbox semantics (one FIFO buffer per process) with round-based communication, where each round consists of a send phase followed by a receive phase with receives matched to sends in the same round. It defines synchronizability as the property that every execution can be rescheduled into an equivalent round-based execution, and shows that deciding whether a system complies with the round-based policy (with no bound on round size) is PSPACE-complete. The proof uses a novel automata construction, which is also applied to determine PSPACE complexity for several related questions from prior literature on fixed-size rounds.

Significance. If the automata constructions are faithful, the result gives the first precise complexity classification for the unbounded-round case in mailbox systems, which is a strict generalization of previous fixed-size round results. The automata method provides a uniform decision procedure that may apply to other synchronizability variants and related verification questions.

major comments (2)
  1. [§4] §4 (automata construction for unbounded rounds): the product construction must be shown to preserve exact equivalence to the original mailbox semantics while allowing arbitrary round sizes; it is unclear whether the state encoding of rounds and the send/receive discipline enforces FIFO ordering and per-round send-receive matching without either bounding rounds implicitly or admitting spurious executions that violate the round-based policy.
  2. [§5] §5 (PSPACE upper bound): the reduction of the synchronizability problem to an automata emptiness or reachability question relies on the construction in §4 being faithful; without an explicit argument that the automata accept precisely the synchronizable executions (including for unbounded rounds), the PSPACE membership claim does not transfer to the original problem.
minor comments (2)
  1. [§2] Notation for mailbox contents and round indices should be introduced with a small example execution to clarify how FIFO order interacts with round boundaries.
  2. The abstract and introduction should explicitly contrast the new unbounded-round result with the fixed-size round results from prior work to highlight the technical novelty.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and the detailed comments on the automata construction. We address the two major comments below and will revise the manuscript to include additional explicit arguments establishing the faithfulness of the construction.

read point-by-point responses

  1. Referee: [§4] §4 (automata construction for unbounded rounds): the product construction must be shown to preserve exact equivalence to the original mailbox semantics while allowing arbitrary round sizes; it is unclear whether the state encoding of rounds and the send/receive discipline enforces FIFO ordering and per-round send-receive matching without either bounding rounds implicitly or admitting spurious executions that violate the round-based policy.

    Authors: The product construction encodes round information and mailbox contents so that transitions respect FIFO order via the per-process buffer simulation and enforce send-receive matching within each round by construction of the product states. Because the state space does not impose an a-priori bound on the number of messages that may be sent before the receive phase of a round, arbitrary round sizes are admitted. We agree that a self-contained lemma explicitly proving language equivalence (no spurious executions and completeness for all synchronizable mailbox executions) is currently only sketched; the revised version will contain this lemma together with the necessary invariants on the state encoding. revision: yes

  2. Referee: [§5] §5 (PSPACE upper bound): the reduction of the synchronizability problem to an automata emptiness or reachability question relies on the construction in §4 being faithful; without an explicit argument that the automata accept precisely the synchronizable executions (including for unbounded rounds), the PSPACE membership claim does not transfer to the original problem.

    Authors: The PSPACE upper bound is obtained by reducing the synchronizability question to emptiness of the product automaton defined in §4. Once the added equivalence lemma establishes that the automaton accepts exactly the synchronizable executions (for unbounded rounds), the reduction is correct and the PSPACE membership follows. Hardness is shown by a separate reduction that does not depend on the automata construction. The revised manuscript will make this dependency explicit by referencing the new lemma in §5. revision: yes

Circularity Check

0 steps flagged

No circularity; standard automata reduction for PSPACE-completeness

full rationale

The paper establishes PSPACE-completeness of synchronizability under unbounded round-based mailbox semantics via a novel automata construction. No self-definitional steps, fitted inputs renamed as predictions, or load-bearing self-citations appear in the derivation chain. The construction is presented as new and directly encodes the round discipline and FIFO mailboxes, with the complexity result following from standard automata decision procedures. This is a self-contained theoretical argument relying on explicit automata encodings rather than any reduction to prior fitted parameters or author-overlapping citations for the core claim.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on standard automata theory for modeling finite-state systems and reductions; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption Finite-state communicating systems with mailbox semantics can be modeled by finite automata.
    Standard modeling assumption in the field of communicating automata.

pith-pipeline@v0.9.0 · 5673 in / 1027 out tokens · 19613 ms · 2026-05-23T23:20:42.780463+00:00 · methodology

discussion (0)

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