pith. sign in

arxiv: 2407.06968 · v7 · 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.

Reference graph

Works this paper leans on

21 extracted references · 21 canonical work pages

  1. [1]

    [BB11] Samik Basu and Tevfik Bultan

    doi:10.1006/INCO.1996.0053. [BB11] Samik Basu and Tevfik Bultan. Choreography conformance via synchronizability. In Proceedings of the 20th International Conference on World Wide Web, WWW 2011, Hyderabad, India, March 28 - April 1, 2011 , pages 795–804. ACM,

    work page doi:10.1006/inco.1996.0053 1996

  2. [2]

    [BB16] Samik Basu and Tevfik Bultan

    doi:10.1145/1963405.1963516. [BB16] Samik Basu and Tevfik Bultan. On deciding synchronizability for asynchronously communicating systems. Theoretical Computer Science, 656:60–75,

    work page doi:10.1145/1963405.1963516

  3. [3]

    com/science/article/pii/S0304397516305102, doi:https://doi.org/10.1016/j.tcs.2016

    URL: https://www.sciencedirect. com/science/article/pii/S0304397516305102, doi:https://doi.org/10.1016/j.tcs.2016. 09.023. [BEJQ18] Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. On the completeness of verifying message passing programs under bounded asynchrony. In Computer Aided Verification - 30th International Conference, CAV 2018, Hel...

    work page doi:10.1016/j.tcs.2016 2016

  4. [4]

    SCInfer: Refinement- Based Verification of Software Countermeasures Against Side- Channel Attacks,

    doi:10.1007/978-3-319-96142-2\_23 . [BGF+21] Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, ´Etienne Lozes, and Amrita Suresh. A unifying framework for deciding synchronizability. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference , volume 203 of LIPIcs, pages 14:1–14:18. Schloss...

    work page doi:10.1007/978-3-319-96142-2 2021

  5. [5]

    [BZ83] Daniel Brand and Pitro Zafiropulo

    doi:10.4230/LIPICS.CONCUR.2021.14. [BZ83] Daniel Brand and Pitro Zafiropulo. On communicating finite-state machines. Journal of the ACM , 30(2):323–342,

    work page doi:10.4230/lipics.concur.2021.14 2021

  6. [6]

    [CS09] Bernadette Charron-Bost and Andr´ e Schiper

    doi:10.1145/322374.322380. [CS09] Bernadette Charron-Bost and Andr´ e Schiper. The Heard-Of model: computing in dis- tributed systems with benign faults. Distributed Computation, 22(1):49–71,

    work page doi:10.1145/322374.322380

  7. [7]

    [DGLP24] Cinzia Di Giusto, Laetitia Laversa, and Kirstin Peters

    doi:10.1007/ S00446-009-0084-6 . [DGLP24] Cinzia Di Giusto, Laetitia Laversa, and Kirstin Peters. Synchronisability in mailbox communica- tion. arXiv preprint arXiv:2411.14580 ,

    work page arXiv

  8. [8]

    Luke Ong

    [DKO13] Emanuele D’Osualdo, Jonathan Kochems, and C.-H. Luke Ong. Automatic verification of erlang- style concurrency. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, SYNCHRONIZABLE MAILBOX COMMUNICATION 25 USA, June 20-22,

    work page 2013

  9. [9]

    [DMS24] Romain Delpy, Anca Muscholl, and Gr´ egoire Sutre

    doi:10.1007/978-3-642-38856-9\_24 . [DMS24] Romain Delpy, Anca Muscholl, and Gr´ egoire Sutre. An automata-based approach for syn- chronizable mailbox communication. In 35th International Conference on Concurrency Theory, CONCUR 2024, September 9-13, 2024, Calgary, Canada , volume 311 of LIPIcs, pages 22:1–22:19. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur I...

    work page doi:10.1007/978-3-642-38856-9 2024

  10. [10]

    [FBS04] Xiang Fu, Tevfik Bultan, and Jianwen Su

    URL: https://doi.org/10.4230/ LIPIcs.CONCUR.2024.22, doi:10.4230/LIPICS.CONCUR.2024.22. [FBS04] Xiang Fu, Tevfik Bultan, and Jianwen Su. Analysis of interacting BPEL web services. In Proceedings of the 13th international conference on World Wide Web, WWW 2004, New York, NY, USA, May 17-20, 2004 , pages 621–630. ACM,

    work page doi:10.4230/lipics.concur.2024.22 2024

  11. [11]

    [FL23] Alain Finkel and ´Etienne Lozes

    doi:10.1145/988672.988756. [FL23] Alain Finkel and ´Etienne Lozes. Synchronizability of communicating finite state machines is not decidable. Logical Methods in Computer Science, 19(4),

    work page doi:10.1145/988672.988756

  12. [12]

    [FS01] Alain Finkel and Philippe Schnoebelen

    URL: https://doi.org/10.46298/ lmcs-19(4:33)2023, doi:10.46298/LMCS-19(4:33)2023. [FS01] Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere!Theoretical Computer Science, 256(1-2):63–92,

    work page doi:10.46298/lmcs-19(4:33)2023 2023

  13. [13]

    [GFLL23] Cinzia Di Giusto, Davide Ferr´ e, Laetitia Laversa, and ´Etienne Lozes

    doi:10.1016/S0304-3975(00)00102-X. [GFLL23] Cinzia Di Giusto, Davide Ferr´ e, Laetitia Laversa, and ´Etienne Lozes. A partial order view of message-passing communication models. Proceedings of the ACM on Programming Languages, 7(POPL):1601–1627,

    work page doi:10.1016/s0304-3975(00)00102-x

  14. [14]

    [GKM07] Blaise Genest, Dietrich Kuske, and Anca Muscholl

    doi:10.1145/3571248. [GKM07] Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae, 80(1-3):147–167,

    work page doi:10.1145/3571248

  15. [15]

    com/articles/fundamenta-informaticae/fi80-1-3-09

    URL: http://content.iospress. com/articles/fundamenta-informaticae/fi80-1-3-09 . [GLL20] Cinzia Di Giusto, Laetitia Laversa, and ´Etienne Lozes. On the k-synchronizability of systems. In Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Pra...

    work page 2020

  16. [16]

    [GLL23] Cinzia Di Giusto, Laetitia Laversa, and ´Etienne Lozes

    doi:10.1007/978-3-030-45231-5\_9 . [GLL23] Cinzia Di Giusto, Laetitia Laversa, and ´Etienne Lozes. Guessing the buffer bound for k- synchronizability. International Journal of Foundations of Computer Science , 34(8):1051–1076,

    work page doi:10.1007/978-3-030-45231-5

  17. [17]

    [GMSZ06] Blaise Genest, Anca Muscholl, Helmut Seidl, and Marc Zeitoun

    doi:10.1142/S0129054122430018. [GMSZ06] Blaise Genest, Anca Muscholl, Helmut Seidl, and Marc Zeitoun. Infinite-state high-level mscs: Model-checking and realizability. Journal of Computer and System Sciences , 72(4):617–647,

    work page doi:10.1142/s0129054122430018

  18. [18]

    [HL00] Lo¨ ıc H´ elou¨ et and Pierre Le Maigat

    doi:10.1016/J.JCSS.2005.09.007. [HL00] Lo¨ ıc H´ elou¨ et and Pierre Le Maigat. Decomposition of message sequence charts. InSAM 2000, 2nd Workshop on SDL and MSC, Col de Porte, Grenoble, France, June 26-28, 2000 , pages 47–60. Verimag, IRISA, SDL Forum,

    work page doi:10.1016/j.jcss.2005.09.007 2005

  19. [19]

    [Lam78] Leslie Lamport

    doi:10.4171/AUTOMATA-2/9. [Lam78] Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM , 21(7):558–565,

    work page doi:10.4171/automata-2/9

  20. [20]

    Time, Clocks, and the Ordering of Events in a Distributed System

    doi:10.1145/359545.359563. [LSWZ23] Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey. Complete multiparty session type projection with automata. In Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III , volume 13966 of Lecture Notes in Computer Science, pages 350–373. Springer,

    work page doi:10.1145/359545.359563 2023

  21. [21]

    Making IP = PSPACE practical: Efficient interactive protocols for BDD algorithms

    doi:10.1007/978-3-031-37709-9\_17 . [MMSZ21] Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. Generalising projection in asynchronous multiparty session types. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference, volume 203 ofLIPIcs, pages 35:1– 35:24. Schloss Dagstuhl - Leibniz-Zen...

    work page doi:10.1007/978-3-031-37709-9 2021