Pith. sign in

REVIEW 4 major objections 6 minor 29 references

On Reconfigurable Bisimulation, with an Application to the Distributed Synthesis Problem

T0 review · 4 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Pith's one-line read A parametric reconfigurable bisimulation lets a centralized transition system be compressed agent-by-agent into smaller asynchronous agents while preserving strong bisimilarity.

desk verdict Novel reconfigurable bisimulation for distributing transition systems, but the main compression theorem is unproved and the summary partition's existence is assumed. read the letter →

arxiv 2505.21672 v1 pith:HSTDHSAY submitted 2025-05-27 cs.LO

classification cs.LO MSC 68Q8568Q60
keywords reconfigurabletransitionsystemsparametricbisimulationdistributedsynthesisasynchronousautomatateamworkcommunication-closedMealymachines
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper claims that a deterministic, communication-closed centralised transition system can be distributed into asynchronous agents that jointly recognise the same language without the state explosion of earlier constructions. The key is to replace a fixed communication scheme with reconfigurable communication: each agent listens to a channel only when it needs information, and disconnects otherwise. The authors introduce parametric reconfigurable bisimulation, prove that compressing each agent with respect to the rest preserves strong bisimilarity, and give a polynomial-time fixpoint algorithm to compute the compression. If correct, the approach also yields a route to distributed synthesis from a global specification by synthesising a single Mealy machine and then distributing it, bypassing the undecidability that fixed communication schemes incur.

What carries the argument

The load-bearing object is the parametric reconfigurable bisimulation: an $E$-indexed family $\{R_\epsilon\}_{\epsilon\in E}$ of relations on the agent's states, where $E$ is the state set of the parameter (the rest of the system) and $f:S\to E$ is the bijection from the trivial decomposition. States are equivalent from the viewpoint of a parameter state only if their labels match and their initiated transitions lead to equivalent states, and crucially condition (2.2)(b)(ii) allows a missing react transition when dropping it does not change the reachable equivalence classes; a uniqueness conjunct forces all such omitted reactions to exit to the same class. The fixed point of the monotone operator $F$ gives the largest such family, and the summary partition merges states that agree from the viewpoint of their companion states, producing the compressed transition system $[T]_C$ by the compression operator of Definition 4.3.

What would settle it

Take a small deterministic communication-closed TS with two agents, compute the largest parametric reconfigurable bisimulation by the paper's fixpoint iteration, and check whether the agreement relation can be partitioned into blocks satisfying Definition 4.2. A single instance where no such summary partition exists, or where the compressed composition is not strongly bisimilar to the original, would disprove Theorem 4.2 and the method's claimed guarantee.

Watch

Extended reading notes

Core claim

The central claim is Theorem 4.2: for a deterministic and communication-closed transition system $T$ trivially decomposed into $T_1$ and $T_2$, compression by reconfigurable bisimulation preserves strong bisimilarity, $(T_1\parallel T_2)\sim([T_1]_{T_2}\parallel[T_2]_{T_1})$. Compression merges states only when they agree from the viewpoint of their companion parameter states and removes react transitions that are not needed; initiate transitions are never removed. The theorem is proved by showing that the largest reconfigurable bisimulation can be computed as the greatest fixed point of a monotone operator, then summarising the parameter-indexed family of equivalence relations into one partition, and then composing the individually compressed agents. The consequence is that agents can be much smaller than the centralised system while the joint behaviour, including branching, is preserved.

Load-bearing premise

The whole argument rests on assuming that a way to lump the agent's states into one partition (satisfying the four listed conditions) exists; the paper does not prove that such a lumping always exists or is unique.

Editorial extensions

If this is right

  • If Theorem 4.2 is correct, each agent can be minimised separately against the rest and the composition of the minimised agents is still strongly bisimilar to the original, so language equivalence and branching behaviour are preserved automatically.
  • The size of each compressed agent is at most the size of the centralised system in the worst case, and in the reported time-sharing case study the largest agent is under a third of the original and the smallest about an eighth.
  • Because react transitions are removed without removing initiate transitions, the method reduces synchronisation directly, so distributed implementations can have only two agents communicating at any moment, with the others not listening.
  • For teamwork synthesis, any realisable global specification over a Mealy machine can be turned into a communication-closed TS, distributed by trivial decomposition, and then compressed, yielding a loosely coupled asynchronous implementation whose language is isomorphic to the specification's language.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The summary partition's maximality condition is the least justified step: the paper proves the theorem for any partition satisfying it but gives no construction, so a natural next test is whether such a partition always exists or whether some communication-closed systems admit no summary partition, leaving Theorem 4.2 conditional on that existence.
  • The same compression idea could be extended to the generalisation listed as future work, where multiple agents may initiate on the same channel; if the agreement relation can be adapted to overlapping interfaces, the asynchrony gained could be larger than in the current disjoint-interface setting.
  • A testable extension is to apply the fixpoint algorithm to stutter-equivalent situations or to specifications given directly as $\omega$-regular automata rather than Mealy machines; the paper's mechanism for deciding when a reaction is unnecessary appears to transfer, provided the state-based listening function is kept intact.
  • The method effectively lets each agent be 'uninformed' whenever its own actions determine the next state, and only becomes partially informed when another agent's choice matters; this suggests a direct connection to epistemic characterisations of distributed knowledge, though the paper only mentions this as a future direction.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

Summary. The paper proposes a method for distributing a deterministic, communication-closed transition system (TS) into several asynchronous agents that together recognize the same language. The method first applies a trivial decomposition (Lemma 3.1) that makes each agent isomorphic to the original system, then compresses each agent with respect to the rest of the system using a new notion of parametric reconfigurable bisimulation (Section 4). The compression is defined through a summary partition of the state space (Definition 4.2) and a compression operator (Definition 4.3). The central claim is Theorem 4.2, stating that the composition of the compressed agents is strongly bisimilar to the original system. The paper also presents a case study of a time-sharing service (Section 5) and an application to a reformulation of distributed synthesis called teamwork synthesis (Section 6).

Significance. If the main theorem were fully established, the paper would offer a genuinely useful alternative to Zielonka-style distribution: the resulting agents can be much smaller than the centralized system, communication interfaces are state-based and reconfigurable, and no fixed communication scheme is required as input. The case study and the prototype tool referenced in Section 7 support the practical relevance of the approach. The teamwork synthesis reformulation is an interesting way to avoid the undecidability of the original distributed synthesis problem, provided it is clearly presented as a different problem rather than a solution to the original one. However, the current manuscript does not contain the necessary existence proof for the summary partition, nor a complete proof of the main composition theorem, and the fixed-point characterization used to compute the bisimulation is not rigorously justified.

major comments (4)
  1. [Section 4, Definition 4.2] The summary partition P is the linchpin of the compression operator (Definition 4.3) and hence of Theorem 4.2, but its existence is never established. The four clauses of Definition 4.2 (Completeness, Disjointness, Consistency, Maximality) are stated as requirements, and the Maximality clause is a non-constructive cardinality inequality with no justification. The paper explicitly notes that the parameter-indexed partitions may disagree (Section 4, paragraph after Lemma 4.2) and gives no algorithm or proof that a single partition P satisfying all four clauses exists for every deterministic communication-closed TS T and parameter C. Without such an existence result, the compressed system [T]_C is undefined, and Theorem 4.2 cannot even be stated for arbitrary T; this is a load-bearing gap.
  2. [Theorem 4.2] The proof of the main theorem is a single sentence: "We prove our main result by reducing each agent with respect to the rest of the composition. The composition of the results is a TS that is bisimilar to the original." This is not a proof. The theorem asserts a strong bisimilarity between two composed systems under a closed-world assumption, which must be made explicit in the statement. A complete proof needs to construct the bisimulation relation between (T1∥T2) and ([T1]_T2∥[T2]_T1), and it must account for the way Definition 4.3 removes react transitions and adds initiate self-loops, as well as for the interaction between the summary partitions of the two agents. Lemma 4.3, which gives the transition-level properties of compressed systems, is also asserted without proof; in particular, Lemma 4.3(1) does not follow directly from the existential condition in Definition 4.3 and requires a separate argument.
  3. [Theorem 4.1, Lemmas 4.1-4.2] The paper does not prove that ∼ϵ is an equivalence relation, and it does not prove that the functional F defined in Section 4 is monotone. Definition 4.1, condition 2.2(b)(ii), contains both positive and negative occurrences of membership in Rϵ; in particular, the closure condition involving "∀s∉{s1,s2} with (s,s2)∈Rϵ" and "(s′,s2)∉Rϵ" is anti-monotone in R. The claim in Lemma 4.2 that F is monotone on the complete lattice of E-indexed relations is therefore non-trivial and currently unsupported. The fixed-point algorithm described in Section 4 and the definition of ∼ϵ as the largest reconfigurable bisimulation depend on this monotonicity. Without a correct proof, the computation of the bisimulation and the construction of the family {∼ϵ} are not justified.
  4. [Section 6, Definition 6.2] The application to distributed synthesis should be framed more carefully as a reformulation. The paper introduces teamwork synthesis as a problem in which the interaction scheme is not part of the input (Definition 6.2), which is indeed a fundamentally different problem from the Pnueli-Rosner distributed synthesis problem. The text acknowledges this in Definition 6.2, but the abstract and conclusion say that distributed synthesis is "bypassed" by dynamic communication pruning, which could mislead readers into thinking that the original undecidable problem is solved. The authors should state unambiguously that the undecidability of the original problem is not contradicted and that the contribution is a new problem formulation with a synthesis algorithm.
minor comments (6)
  1. [Definition 2.3] There is a typo: "strong bisimulatin" should be "strong bisimulation."
  2. [Lemma 3.1] The proof says each Tk is isomorphic to T, but the states of Tk are labeled by projected labels. This is an isomorphism of the underlying transition structure, not of labeled transition systems; the wording should be clarified.
  3. [Section 4, after Lemma 4.2] The displayed fixed-point equation is malformed and duplicated: it reads "Fhas a maximal fixed point, equivalent to ⋃{R|R⊆F(R)}⋃{R|R⊆F(R)}={∼ ϵ}ϵ∈E". This should be corrected.
  4. [Section 4, Definition 4.2(3.b)] The Maximality condition uses a cardinality inequality that is never explained. The authors should provide intuition or a derivation showing why this condition is necessary for the correctness of the compression operator.
  5. [Section 5] The statement that "using traditional bisimulation techniques would almost result in zero reduction" is made without supporting data or a formal comparison. Either provide a concrete comparison or soften the claim.
  6. [Theorem 4.2] The closed-world assumption is only mentioned after the theorem statement. It should be incorporated into the statement of the theorem so that the result is unambiguous.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the central compression theorem is an under-proved mathematical claim, not a reduction to the paper's own definitions or a fitted parameter.

full rationale

The derivation is definitional in the benign sense: Def 2.1 fixes the TS model, Def 2.3 fixes strong bisimilarity, Def 4.1 defines reconfigurable bisimulation as the greatest fixed point of the monotone operator F (Lemma 4.2), Def 4.2 fixes the summary partition P by Completeness, Disjointness, Consistency and Maximality, and Def 4.3 constructs the compressed system [T]_C from P. Theorem 4.2 then states a property of this construction - (T1||T2) ~ ([T1]_T2 || [T2]_T1) - rather than restating the definition. The reconfigurable bisimulation is computed by fixpoint iteration, not fitted to the goal equivalence, and the maximality condition in Def 4.2 is a substantive (if opaque) well-definedness requirement, not the theorem's conclusion. Self-citations [4,5] motivate the reconfigurable semantics but Def 2.1 is self-contained, and Lemma 2.1 relies on the external congruence result [18]. The genuine weakness is that Theorem 4.2 is only sketched ('We prove our main result by reducing each agent with respect to the rest of the composition') and no existence or algorithm for a partition P satisfying all four clauses is provided; in particular the cardinality inequality in the Maximality clause is not derived. A missing proof is a correctness/completeness gap, not circular reasoning. No step reduces, by equation or by self-citation chain, to its own input, so no circular step is exhibited.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The central result rests on the unproved existence of the summary partition and the omitted proof of Theorem 4.2; there are no numerically fitted parameters.

assumptions (3)
  • standard math Tarski fixed point theorem for monotone functions on complete lattices
    Used in Lemma 4.2 to obtain the maximal fixed point of F; standard background.
  • ad hoc to paper Existence of a summary partition P satisfying Definition 4.2
    The compression operator and Theorem 4.2 require a partition meeting completeness, disjointness, consistency, and maximality; no existence proof or construction is given.
  • domain assumption Closed-world assumption in Theorem 4.2
    The theorem considers only communications initiated within the system and ignores external ones; the proof sketch relies on this scoping.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On Reconfigurable Bisimulation, with an Application to the Distributed Synthesis Problem." pith.science (2026). https://pith.science/paper/HSTDHSAY

@misc{pith2026250521672,
  author       = {Pith},
  title        = {Pith review of: On Reconfigurable Bisimulation, with an Application to the Distributed Synthesis Problem},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HSTDHSAY}},
  note         = {Machine review of arXiv:2505.21672}
}
read the original abstract

We consider the problem of distributing a centralised transition system to a set of asynchronous agents recognising the same language. Existing solutions are either manual or involve a huge explosion in the number of states from the centralised system. The difficulty arises from the need to keep a rigid communication scheme, specifying a fixed mapping from events to those who can participate in them. Thus, individual agents need to memorise seen events and their order to dynamically compare their knowledge with others when communicating. To bypass this, we rely on reconfigurable communication: agents decide locally ``by-need'' when to participate or discard specific events during execution while not impacting the progress of the joint computation. Our distribution relies on a novel notion of Parametric Reconfigurable Bisimulation, that identifies the only required participations. We show how to compute this bisimulation and that such minimisation produces a joint system that is bisimilar to the original centralised one. We use a case study to show its effectiveness by producing agents that are much smaller than the centralised system and jointly perform the same computations. As a notable application, we use this distribution in order to allow for distributed synthesis from global specifications. In this case, rigid communication leads to undecidability, which is bypassed by our ability to dynamically prune communications.

Figures

Figures reproduced from arXiv: 2505.21672 by the authors.

Figure 5
Figure 5. Time-sharing service (distributed) reduction of the state-space in the TS decomposition problem we consider in this paper. This is because all transitions before and after the trivial composition have potentials to be composed with others. That is, they are either of type reaction (receive) or initiation (send), and we do not have any hidden (τ ) transitions, that existing notions can reduce. Reconfigurable bisimula… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

29 extracted references · 15 canonical work pages

  1. [1]

    A distributed coordination infrastructure for attribute-based interaction

    Yehia Abd Alrahman , Rocco De Nicola , Giulio Garbi, and Michele Loreti. A distributed coordination infrastructure for attribute-based interaction. In Formal Techniques for Distributed Objects, Components, and Systems - 38th IFIP WG 6.1 International Conference, FORTE 2018, Held as Part of the 13th International Federated Conference on Distributed Computi...

  2. [2]

    On the power of attribute-based communication

    Yehia Abd Alrahman , Rocco De Nicola , and Michele Loreti. On the power of attribute-based communication. In Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion, C...

  3. [3]

    A calculus for collective-adaptive systems and its behavioural theory

    Yehia Abd Alrahman , Rocco De Nicola , and Michele Loreti. A calculus for collective-adaptive systems and its behavioural theory. Inf. Comput. , 268, 2019. https://doi.org/10.1016/j.ic.2019.104457 doi:10.1016/j.ic.2019.104457

  4. [4]

    A PO characterisation of reconfiguration

    Yehia Abd Alrahman , Mauricio Martel, and Nir Piterman. A PO characterisation of reconfiguration. In Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu, editors, Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings , volume 13572 of Lecture Notes in Computer Science , pages 42-...

  5. [5]

    Modelling and verification of reconfigurable multi-agent systems

    Yehia Abd Alrahman and Nir Piterman. Modelling and verification of reconfigurable multi-agent systems. Auton. Agents Multi Agent Syst. , 35(2):47, 2021. https://doi.org/10.1007/s10458-021-09521-x doi:10.1007/s10458-021-09521-x

  6. [6]

    Programming interactions in collective adaptive systems by relying on attribute-based communication

    Yehia Abd Alrahman, Rocco De Nicola, and Michele Loreti. Programming interactions in collective adaptive systems by relying on attribute-based communication. Sci. Comput. Program. , 192:102428, 2020. https://doi.org/10.1016/j.scico.2020.102428 doi:10.1016/j.scico.2020.102428

  7. [7]

    Bisimulation can't be traced

    Bard Bloom, Sorin Istrail, and Albert R Meyer. Bisimulation can't be traced. Journal of the ACM (JACM) , 42(1):232--268, 1995

  8. [8]

    Distributed bisimulations

    Ilaria Castellani and Matthew Hennessy. Distributed bisimulations. J. ACM , 36(4):887--911, 1989. https://doi.org/10.1145/76359.76369 doi:10.1145/76359.76369

Show all 29 references
  1. [9]

    Henzinger, and Nir Piterman

    Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. Inf. Comput. , 208(6):677--693, jun 2010. https://doi.org/10.1016/j.ic.2009.07.004 doi:10.1016/j.ic.2009.07.004

  2. [10]

    Halpern, Yoram Moses, and Moshe Y

    Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning about Knowledge. MIT Press, 1995

  3. [11]

    Uniform distributed synthesis

    Bernd Finkbeiner and Sven Schewe. Uniform distributed synthesis. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings , pages 321--330. IEEE Computer Society, 2005. https://doi.org/10.1109/LICS.2005.53 doi:10.1109/LICS.2005.53

  4. [12]

    Optimal zielonka-type construction of deterministic asynchronous automata

    Blaise Genest, Hugo Gimbert, Anca Muscholl, and Igor Walukiewicz. Optimal zielonka-type construction of deterministic asynchronous automata. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages a...

  5. [13]

    Distributed controller synthesis for deadlock avoidance

    Hugo Gimbert, Corto Mascle, Anca Muscholl, and Igor Walukiewicz. Distributed controller synthesis for deadlock avoidance. In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, ...

  6. [14]

    Pascal Gribomont

    Paul Gochet and E. Pascal Gribomont. Epistemic logic. In Logic and the Modalities in the Twentieth Century , pages 99--195. 2006. https://doi.org/10.1016/S1874-5857(06)80028-2 doi:10.1016/S1874-5857(06)80028-2

  7. [15]

    C. A. R. Hoare. Communicating sequential processes. In Cliff B. Jones and Jayadev Misra, editors, Theories of Programming: The Life and Works of Tony Hoare , pages 157--186. ACM / Morgan & Claypool, 2021. https://doi.org/10.1145/3477355.3477364 doi:10.1145/3477355.3477364

  8. [16]

    A quadratic construction for Zielonka automata with acyclic communication structure

    Siddharth Krishna and Anca Muscholl. A quadratic construction for Zielonka automata with acyclic communication structure. Theor. Comput. Sci. , 503:109--114, 2013. https://doi.org/10.1016/j.tcs.2013.07.015 doi:10.1016/j.tcs.2013.07.015

  9. [17]

    A context dependent equivalence between processes

    Kim Guldstrand Larsen. A context dependent equivalence between processes. Theor. Comput. Sci. , 49:184--215, 1987. https://doi.org/10.1016/0304-3975(87)90007-7 doi:10.1016/0304-3975(87)90007-7

  10. [18]

    Deriving bisimulation congruences for reactive systems

    James J Leifer and Robin Milner. Deriving bisimulation congruences for reactive systems. In International Conference on Concurrency Theory , pages 243--258. Springer, 2000

  11. [19]

    Barbed bisimulation

    Robin Milner and Davide Sangiorgi. Barbed bisimulation. In Werner Kuich, editor, Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings , volume 623 of Lecture Notes in Computer Science , pages 685--695. Spri...

  12. [20]

    Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning About Strategies: On the Model-Checking Problem. volume 15, 2014. doi:10.1145/2631917

  13. [21]

    Madhavan Mukund and Milind A. Sohoni. Keeping track of the latest gossip in a distributed system. Distributed Comput. , 10(3):137--148, 1997. https://doi.org/10.1007/S004460050031 doi:10.1007/S004460050031

  14. [22]

    Automated synthesis of distributed controllers

    Anca Muscholl. Automated synthesis of distributed controllers. In Magn \' u s M. Halld \' o rsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Pro...

  15. [23]

    Vaandrager

    Rocco De Nicola and Frits W. Vaandrager. Three logics for branching bisimulation. J. ACM , 42(2):458--487, 1995. https://doi.org/10.1145/201019.201032 doi:10.1145/201019.201032

  16. [24]

    Distributed reactive systems are hard to synthesize

    Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, October 22-24, 1990, Volume II , pages 746--757. IEEE Computer Society, 1990. https://doi.org/10.1109/FSCS.1...

  17. [25]

    The control of discrete event systems

    P.J.G Ramadge and W.M Wonham. The control of discrete event systems . Proceedings of the IEEE , 77(1):81--98, 1989. https://doi.org/10.1109/5.21072 doi:10.1109/5.21072

  18. [26]

    A theory of bisimulation for the pi-calculus

    Davide Sangiorgi. A theory of bisimulation for the pi-calculus. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings , volume 715 of Lecture Notes in Computer Science , pages 127--142. Spring...

  19. [27]

    Synthesis of distributed algorithms using asynchronous automata

    Alin Stefanescu, Javier Esparza, and Anca Muscholl. Synthesis of distributed algorithms using asynchronous automata. In Roberto M. Amadio and Denis Lugiez, editors, CONCUR 2003 - Concurrency Theory, 14th International Conference, Marseille, France, September 3-5, 2003, Proceed...

  20. [28]

    van Glabbeek and W

    Rob J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics. J. ACM , 43(3):555--600, 1996. https://doi.org/10.1145/233551.233556 doi:10.1145/233551.233556

  21. [29]

    Notes on finite asynchronous automata

    Wieslaw Zielonka. Notes on finite asynchronous automata. RAIRO Theor. Informatics Appl. , 21(2):99--135, 1987. https://doi.org/10.1051/ita/1987210200991 doi:10.1051/ita/1987210200991

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.