{"id":"772a4da1-5de9-4e49-bf9d-c5b07af4ca21","arxiv_id":"1908.08637","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Immediate observation mediated population protocols can simulate all population protocols and thus compute every semilinear predicate.","lead":"This paper shows that mediated population protocols with one-way immediate observation can compute every predicate that the original two-way population protocol model can compute. The result suggests that two-way communication is not essential when agents can store information on the edges between them.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 21 is false as stated: for P with transition (1,0)->(0,1), C=(1,0) is output-stable in P but [C] is not output-stable in P'; Theorem 22's proof relies on this lemma.","rationale":"The paper's central claim is that IOMPP can compute every semilinear predicate, proven by constructing P' and showing operational correspondence, I/O correspondence, and output stability preservation. The most load-bearing step is Lemma 21, which asserts the translation preserves output stability for any population protocol. This lemma is demonstrably false as stated: the simple protocol with a single transition (1,0)->(0,1) has an output-stable configuration C=(1,0) whose translation is not output-stable in P', because t(1) can make both agents output 1. This is not merely a missing detail; it is a concrete counterexample to a lemma used directly in Theorem 22. The reader's verdict accepted the proof with moderate confidence, noting that the operational soundness and output stability proofs are sketchy, but did not identify this concrete failure. The main theorem may still be true for well-specified predicate-computing protocols, since those never have reachable output-stable configurations with mixed outputs, and uniform output-stable configurations cannot enable output-changing transitions. However, as written the proof is unsound: Lemma 21 must be corrected (e.g., restricted to uniform-output stable configurations or paired with a proper treatment of the abort path) before Theorem 22 follows. Therefore the appropriate verdict is conditional acceptance pending this correction, rather than unconditional acceptance.","tokens_in":12933,"tokens_out":31353,"duration_ms":285419,"concrete_test":"Build P with Q={0,1}, Σ={0,1}, I=id, O(0)=0, O(1)=1, δ={(1,0)->(0,1)}. Simulate it with Simulation 10. Take the two-agent configuration C=(1,0). Check that (i) in P the only reachable configurations from C are (1,0) and (0,1), both mixed, so C is output-stable with output ⊥; and (ii) in P' the transition t(1) with ordered pair ((U,1),(U,0)) is enabled and leads to states ((U,1),(L,1)) with edge (2,1)=0, where both agents have output 1. This demonstrates O'([C])=⊥ but a reachable configuration with output 1, refuting Lemma 21. A corrected proof must restrict output-stability preservation to configurations that are output-stable with a uniform output (the case relevant to predicate computation) and handle the t(1)-then-t(5) abort path.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Lemma 21 claims the translation is output-stability preserving for any population protocol P. This is refuted by a simple example. Let Q={0,1}, O(0)=0, O(1)=1, and δ={(1,0)->(0,1)}. Consider C=(1,0), a two-agent population. Reachable configurations from C are C itself and (0,1); both have one agent with output 1 and one with output 0, so O(C)=⊥ and every reachable configuration has output ⊥. Thus C is output-stable in P. In the simulated P', the translated configuration [C]=((U,1),(U,0)) can take transition t(1) for t=(1,0)->(0,1): ((U,1),sinit,(U,0),sinit) -> ((U,1),sinit,(L,1),0). After this step both agents have computation state 1, so the global output is 1 (all agents output 1), which differs from O'([C])=⊥. Hence [C] is not output-stable in P'. This contradicts Lemma 21. Since Lemma 21 is invoked in Theorem 22 via Lemma 18, the proof of the central expressiveness claim is unsound as written. The gap in the lemma's proof is the abort case: if the first output-changing transition is t(1) and the conversation later aborts via t(5), the agent's output reverts, so the constructed C' may equal C and no contradiction arises.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper defines immediate observation mediated population protocols (IOMPP), combining the edge storage of mediated population protocols with one-way immediate observation communication, and claims that IOMPP can compute every semilinear predicate and are therefore at least as expressive as standard population protocols (Corollary 23). The proof is constructive: for any population protocol P, the authors build an IOMPP P' (Simulation 10) that simulates each two-way interaction by a four-step handshake with an abort/reset transition, define a configuration translation (Definition 14), and then establish operational correspondence (Lemma 19), input/output correspondence (Lemma 20), and output stability preservation (Lemma 21), from which they derive the expressiveness result via Lemma 18. The paper also outlines a similar simulation for mediated population protocols and conjectures that IOMPP are as expressive as MPP (Section 4.3).","tokens_in":13218,"tokens_out":27954,"duration_ms":272693,"significance":"Conditional on the proof gaps being repaired, this is a solid contribution: it shows that the immediate observation restriction does not cost expressiveness relative to population protocols once edge states are available, and the proposed simulation technique, adapting Gorla's encodability criteria to population protocols, is reusable and gives additional preservation properties (livelock freedom, interaction graph support, and a discussion of fault tolerance). The construction is explicit and the main lemmas are plausible; no circularity is present. The conjectured extension to full MPP expressiveness is well-motivated and would be a sharp characterization if proven. However, the manuscript is not yet at journal standard because two load-bearing proof steps are incomplete (see major comments).","major_comments":[{"comment":"The proof of the forward direction of Lemma 21 is incorrect for the case in which the first output-changing transition is of type (1). In that case the configuration C′ constructed as in Lemma 19 from the configuration D after the t(1) step is exactly C (the conversation has not reached a t(2), and the cleanup path from D to [C′] uses t(5), making agent a the observer of a type-(5) transition). The statement in the proof that \"agent a is never an observer of any transition with type (1), (2), or (5)\" on the path from D to [C′] is therefore false, and the displayed chain of equalities from O((C)_a) to O((C′)_a) does not hold. The lemma is nevertheless true: if a t(1) changes the output of its observer, then the corresponding original transition (p,q) → (p′,q′) is enabled in C and changes the output of the responder in P, contradicting output stability of C. This argument should replace the current construction for the t(1) case. Note also that the alleged counterexample with P having transition (1,0) → (0,1) and C = (1,0) does not refute the lemma, since O(C) = ⊥ and C is not output-stable under Definition 4.","section":"4.2, Lemma 21"},{"comment":"Lemma 18 does not, as written, prove that P and P′ compute the same predicate, because it does not transfer the well-specifiedness condition. The proof asserts, without proof, that \"a configuration is reachable from an initial configuration in P′ iff it has a corresponding configuration reachable from the corresponding initial configuration in P\", which is stronger than the operational correspondence actually defined (soundness provides, for each reachable D, some C′ with D →* [C′] and C →* C′, not an iff). More importantly, no argument shows that every fair execution of P′ reaches an output-stable configuration; one must prove that the sequence of t(2) steps extracted from a fair execution of P′ yields a fair execution of P (using Observation 12, Observation 13, and the finite-state/fairness argument), and the paper omits this. Since Theorem 22 invokes Lemma 18, this gap is load-bearing for the main expressiveness claim, although it appears fixable with a dedicated fairness lemma.","section":"4.1, Lemma 18"}],"minor_comments":[{"comment":"The phrase \"We also making use of a set representation\" should read \"We also make use of a set representation\".","section":"2, Definition 9 (and Definition 2)"},{"comment":"The t(4) rule is written \"for every (x,y) ∈ Q′\" but the resulting state (U,p′) depends on the original transition t; the dependency should be made explicit to avoid ambiguity.","section":"3.1, Simulation 10"},{"comment":"The cleanup order in the operational-soundness proof is justified only informally; the authors should state why, after applying t(3) in the first case (D_{i,j} = q and D_{j,i} = sponr), the subsequent t(4) is enabled and why no other pending conversation can interfere.","section":"4.2, proof of Lemma 19"},{"comment":"References [7] and [8] appear to be duplicate entries for the same Das et al. paper \"Mediated Population Protocols: Leader Election and Applications\"; one should be removed.","section":"References"},{"comment":"Conjecture 26 is clearly labeled as a conjecture, but the sentence \"The proof of our Conjecture 26 can hopefully be done in our future research\" could be more precise about what has been verified so far, since the simulation's transition definitions are given but no correspondence lemmas are claimed for it.","section":"4.3, Conjecture 26"}],"recommendation":"major_revision","confidential_remarks":"The paper is a workshop-style contribution with a promising construction, but the proof of the main theorem is not yet rigorous enough for a journal. The central claim is likely correct, but the two gaps identified above must be addressed and the proofs expanded. The alleged counterexample to Lemma 21 circulated with the manuscript is not valid under the paper's own definition of output stability; the required correction is a different, and smaller, repair to the proof."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper proves something real: immediate observation mediated population protocols can simulate every ordinary population protocol, so they compute every semilinear predicate. The construction is the interesting part—the lock/unlock handshake with edge-state backups, plus the transfer of Gorla's operational correspondence criteria to this setting. To my knowledge this is not in the earlier literature, and the simulation is explicitly constructive rather than an existence claim. The claimed expressiveness equivalence is plausible and the proof strategy is sound in outline.\n\nThe weak spot is not the main idea but the rigor of the proofs. Lemma 19's operational soundness argument is compressed: the construction of C' from edge states and the claim that the cleanup transitions always lead to a translated configuration are believable, but the invariant that backs it (no agent participates in two started conversations, and every t(2) is eventually resolved) is only sketched. Lemma 21 is also terse, especially the abort case for t(5). A fully formal version would need to spell out why aborted conversations leave edge states clean and why the reconstructed original configuration is reachable. These are fixable gaps, not fatal flaws.\n\nI specifically checked the stress-test note alleging that Lemma 21 is false. That counterexample fails. In the example P with transition (1,0)->(0,1), the configuration C=(1,0) always has mixed outputs, so O(C)=⊥ on every reachable configuration. Under the paper's Definition 4, output stability requires a stable output x∈{0,1}, so C is not output stable in P. The alleged mismatch between P and P' therefore does not arise. The stress-test reading is incorrect, and the lemma's proof, while sketchy, is not refuted by that example.\n\nThe citation pattern looks fine: the paper builds on Angluin et al., Michail et al., and Gorla, and the new contribution is clearly separated. No circularity or data issues—this is a theory paper with no experimental component.\n\nWho is this for? Researchers working on population protocol variants, expressiveness hierarchies, and encoding-based proofs in distributed computing. It is a workshop-level contribution—the core idea is noteworthy, but the presentation would benefit from more detailed proofs. I would send it to a serious referee for a workshop or a short conference track, not desk-reject it. With fuller proofs it could also survive a stronger venue. My verdict: accept, with encouragement to tighten the lemmas.\n\nI would bring it to a distributed systems reading group, and I would cite it if I published on population protocol expressiveness in the next year.","headline":"A solid, genuinely new expressiveness result for mediated population protocols; the stress-test counterexample to Lemma 21 does not hold up because it misreads the definition of output stability.","tokens_in":13719,"tokens_out":4878,"would_cite":true,"duration_ms":50496,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q10","68Q85"],"pacs":[],"model":"deepseek-v4-flash","headline":"Immediate-observation mediated population protocols can compute every semilinear predicate.","keywords":["population protocols","immediate observation","mediated population protocols","semilinear predicates","operational correspondence","simulation","anonymous agents","asynchronous communication"],"falsifier":"Run an exhaustive reachability search on a small population protocol (for instance, a two-agent or three-agent majority or parity protocol) and its Simulation-10 IOMPP; if any reachable simulated configuration cannot be returned to a translated configuration of the original protocol by the prescribed clean-up transitions, or if a fair execution stabilizes to the wrong output, the claim fails. A concrete witness would be a reachable edge state holding a backup value while the partner's edge slot holds sponr, with no enabled transition to clear it.","tokens_in":12751,"feed_emoji":"","tokens_out":5739,"duration_ms":54094,"temperature":0.7,"pith_summary":"The paper sets out to show that immediate observation—a one-way, asynchronous form of communication in which an agent can see a partner's state without the partner changing—does not weaken population protocols once agents also have access to edge memory. The central result is that every population protocol can be translated into an immediate-observation mediated population protocol (IOMPP) that computes the same predicate. Because population protocols are known to compute exactly the semilinear predicates, this means IOMPPs can compute every semilinear predicate and are at least as expressive as the basic model. A sympathetic reader should care because the translation is generic: it preserves not only the computed predicate but also properties such as reachability structure and livelock behaviour, and the authors conjecture the same technique can show immediate observation is no restriction at all for mediated population protocols.","feed_headline":"One-way observation matches full population-protocol power","feed_subtitle":"With edge memory, one-way asynchronous agents compute every semilinear predicate.","key_machinery":"The load-bearing object is the simulation protocol of Simulation 10, which splits each two-way transition into four one-way steps plus an abort. Each agent carries a lock/unlock flag and a computation state; each edge has two memory slots, one per endpoint, initialized to a neutral state. The edge slot acts as both a request channel and a backup of the pre-communication state, enabling a clean rollback via transition t(5) when a handshake breaks. The proof additionally relies on the triple of translation criteria—operational completeness and soundness, input/output correspondence, and output-stability preservation—adapted from process-calculus encodability, which together guarantee the simulated and original protocols compute the same predicate.","core_discovery":"The paper's claim, on its own terms, is that immediate-observation mediated population protocols have the full computational power of ordinary population protocols. The proof works by simulating any two-way communication as a four-step, one-way handshake: a potential responder locks itself, writes its old state into the edge as a backup, and signals interest; the initiator acknowledges by locking itself and writing an acknowledgement; the two then unlock and restore the edge states in the correct order. A fifth, abort transition restores the state if the handshake fails. A translation from population-protocol configurations to IOMPP configurations, together with operational correspondence, input/output correspondence, and output-stability preservation, shows the simulation computes exactly the predicate of the original protocol. The authors state this as Theorem 22 and draw the corollary that IOMPPs compute every semilinear predicate.","pith_inferences":["The simulation slows each two-way interaction by a constant factor of four, so asymptotic time-complexity bounds for population protocols should transfer to IOMPPs up to a constant factor; the paper does not discuss this explicitly.","The same four-step handshake plus abort pattern could serve as a general building block for compiling synchronous or two-way protocols onto purely asymmetric, asynchronous communication models beyond population protocols.","If Conjecture 26 is proved, it would imply that the entire mediated population protocol hierarchy collapses: edge memory is sufficient and two-way communication is merely a syntactic convenience.","The use of operational correspondence as a proof technique may extend naturally to other protocol variants—for example, protocols with different edge-state initializations or non-complete interaction graphs—where a direct simulation argument would be harder."],"forward_implications":["Every predicate computable by population protocols—i.e., every semilinear predicate—is computable by IOMPPs (Corollary 23).","The simulation preserves the structure of executions: any reachable configuration of the original protocol corresponds to a reachable configuration of the simulation, and vice versa, so properties like livelock freedom carry over.","If the conjecture holds, the full mediated population protocol model, with two-way communication, is exactly as expressive as the immediate-observation version, and two-way communication is not computationally necessary.","The construction is generic, so any population protocol can be translated without losing the desirable properties the authors identify: livelock freedom, support by the same interaction graphs, and partially failure resistance."],"supporting_citations":[{"why":"Establishes that population protocols compute exactly the semilinear predicates, providing the target class the simulation must match.","marker":"[4]"},{"why":"Supplies the operational correspondence criteria that the translated simulation must satisfy to preserve computation.","marker":"[11]"},{"why":"Introduces mediated population protocols with edge states, the model that immediate observation is added to in this paper.","marker":"[12]"},{"why":"Gives the standard definition of population protocols and their global computation semantics used as the simulation source.","marker":"[6]"}],"fun_headline_variants":["One-way observation matches full population-protocol power","Immediate observation with edge memory equals classic PP power","Four-step one-way handshake simulates two-way in PP","Edge memory lets one-way agents compute all semilinear predicates","IOMPP: one-way observation proves as strong as standard PP"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof assumes that every conversation started in the simulation either reaches the acknowledgement and then completes, or is cleanly aborted by the reset transition, and that aborts always leave both agents unlocked and all edge states back to neutral; the soundness proof only sketches why this invariant holds.","fun_headline_variants_meta":{"raw":{"variants":["One-way observation matches full population-protocol power","Immediate observation with edge memory equals classic PP power","Four-step one-way handshake simulates two-way in PP","Edge memory lets one-way agents compute all semilinear predicates","IOMPP: one-way observation proves as strong as standard PP"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000621,"raw_usage":{"total_tokens":2856,"prompt_tokens":903,"completion_tokens":1953,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":519,"completion_tokens_details":{"reasoning_tokens":1872}},"tokens_in":519,"tokens_out":1953,"duration_ms":14791,"temperature":1.0,"reasoning_tokens":1872,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T11:36:18.204018+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run an exhaustive reachability search on a small population protocol (for instance, a two-agent or three-agent majority or parity protocol) and its Simulation-10 IOMPP; if any reachable simulated configuration cannot be returned to a translated configuration of the original protocol by the prescribed clean-up transitions, or if a fair execution stabilizes to the wrong output, the claim fails. A concrete witness would be a reachable edge state holding a backup value while the partner's edge slot holds sponr, with no enabled transition to clear it.","supporting_citations":[],"review_version":1}