{"id":"d663bf5b-13d5-4a7a-9196-6de3113e6a89","arxiv_id":"1908.03489","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":4,"one_line_summary":"A Persistent Entropy Automaton is given operational semantics and augmented into a monitor, then applied to 1000 simulated immune-system traces to produce descriptive event-pattern classes rather than validated temporal invariants.","lead":"The paper defines a formal monitor, the MPEA, that turns topological measurements of a system's changing data into an automaton and checks execution traces against temporal properties. It applies this monitor to a simulated human immune system, reporting that most simulated runs reach an immune-memory state while a small fraction do not.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The central claim that the monitor reveals temporal properties needed for immunization memory is unsupported: trace labels and example properties derive from hand-assigned PE plateaus and an explicitly unobserved self-loop, with no ground-truth comparison.","rationale":"The formal contribution -- PEA, PELTS, MPEA -- is internally coherent, and I see no bug in the four transition rules. The problem is that the advertised run-time monitoring result rests on a labeling step done by hand on the smoothed PE chart, including a self-loop that the text explicitly says was not observed. Since the trace classes and the three example properties are all read off from MPEA executions, an error in that labeling automatically invalidates the empirical claim. The paper also stops short of actually mining or statistically testing the properties: no threshold analysis, no precision/recall, no comparison with simulator ground truth. This matches the reader's REJECT verdict, so I recommend no change. A single held-out comparison with direct C-ImmSim memory indicators would settle whether the hand-assigned equilibrium conditions and the unobserved virgin self-loop are legitimate modeling choices or the source of the reported classification.","tokens_in":15479,"tokens_out":6430,"duration_ms":75353,"concrete_test":"Re-analyze the 1000 simulated runs with a direct ground-truth label from C-ImmSim: for each run, record whether the simulator itself reports immune memory (e.g., presence of long-lived memory cells at the final tick or a successful secondary response). Then run the MPEA on the corresponding PET and construct a confusion matrix between the MPEA final label (virgin/memory/omega) and the direct label, and separately compute how many ground-truth memory runs satisfy property 2 (2<=2190(((virgin or memory) and next omega) implies eventually<=180 memory)).","verdict_should_be":"UNCHANGED","load_bearing_attack":"To support the abstract's claim, the MPEA must (1) assign steady states that faithfully correspond to immune-memory outcomes, and (2) actually evaluate the suggested bounded-LTL properties on the traces. Neither is demonstrated. Section 4.1 fixes virgin and memory by visual inspection of a smoothed PE plot (H=0 with Hdot=0 and H>0 with Hdot=0), adds a memory self-loop from the shape of the second peak, and adds a virgin self-loop that the authors state was not observed, using 'domain specific knowledge.' The entire trace classification of Section 5.1 (198/780/22) is produced by running that MPEA, so any mis-specification of these conditions propagates directly into the claimed groups and the example properties. Moreover, the paper does not compare MPEA verdicts with any independent C-ImmSim indicator of immune memory (e.g., memory-cell counts or secondary-response success), and the three bounded-LTL formulas in Section 5.1 are presented as 'examples of properties that could be run-time verified,' not as invariants mined from the 1000 traces with statistical support. The formal PELTS semantics is coherent, but the empirical separation claim is therefore not established.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a data-driven runtime monitoring framework for complex systems. It defines Persistent Entropy Automata (PEA) and their operational semantics as Persistent Entropy Labelled Transition Systems (PELTS), then augments PEAs into Monitor PEAs (MPEAs) that consume time-stamped persistent-entropy traces and emit traces of atomic propositions. The method is applied to simulated data from the C-ImmSim immune-system model, where the authors report that MPEA execution over 1000 traces yields three trace groups (198 ending in virgin, 780 ending in memory, 22 ending in an incomplete transition), and they list three bounded-LTL properties as examples of invariants that could be verified. The abstract claims that the monitor 'reveals temporal properties that should be satisfied in order to reach immunization memory.'  The formal PELTS semantics is the paper's main technical contribution; the empirical support for the central claim is the main weakness.","tokens_in":15726,"tokens_out":6348,"duration_ms":68134,"significance":"If the empirical claim were established, the paper would offer a genuinely useful bridge between topological data analysis and runtime verification: component-level observations, summarized by persistent entropy, are used to build an automaton-level monitor for a global system property. The formal definitions of PELTS and MPEA are largely coherent and provide a reusable semantic basis for this idea. The paper also honestly exposes its own construction choices, including a self-loop added from domain knowledge. However, the load-bearing empirical demonstration is not currently supported: the PEA states are hand-assigned from a smoothed plot, no ground-truth comparison is made with C-ImmSim's own immune-memory indicators, and the proposed LTL properties are presented only as examples rather than as statistically mined and verified invariants. The formal framework also contains a codomain error for persistent entropy values. These issues can, in principle, be repaired with additional experiments and a tightened specification, so the paper warrants revision rather than outright rejection.","major_comments":[{"comment":"The MPEA states and transitions are not mined in a reproducible way. Section 4.1 fixes the virgin condition H=0 ∧ Hdot=0 and the memory condition H>0 ∧ Hdot=0 by visual inspection of a smoothed PE plot, and it adds the virgin self-loop 'even if we did not observe it in our simulation' from domain knowledge. Since the entire trace classification of Section 5.1 (198/780/22) is generated by executing this MPEA, any mis-specification of these equilibrium conditions propagates directly into all group counts and all example properties. The paper should replace these hand-assigned conditions with an explicit algorithmic plateau-detection and steady-state identification procedure, including its parameters, or the empirical claims cannot be audited.","section":"Section 4.1 and 5.1"},{"comment":"No independent ground truth is used to validate the MPEA verdicts. Section 3.2 states that C-ImmSim implements immune memory as a cell state with increased half-life, which provides direct indicators (e.g., memory-cell counts or secondary-response kinetics), but the paper never compares the MPEA classifications with any such indicator. Without this comparison, the abstract's claim that the monitor 'reveals temporal properties that should be satisfied in order to reach immunization memory' is not established. At minimum, the authors should report the agreement between MPEA trace groups and C-ImmSim's own memory markers, e.g., precision and recall of the memory classification.","section":"Section 5.1 / 3.2"},{"comment":"The three bounded-LTL formulas are introduced as 'examples of properties that could be run-time verified' and as 'possible properties', not as invariants mined from the 1000 traces with statistical support. The paper does not report satisfaction rates per trace group, confidence intervals, or any test of whether the properties separate groups I, II, and III. The central claim requires actually evaluating the inferred properties on all traces and showing that they hold on memory traces and fail on non-memory traces. As written, no property is evaluated on any trace.","section":"Section 5.1"},{"comment":"Definitions 4.4 and 4.5 place PE values in the interval R[0,1], but the persistent entropy of Definition 2.1 ranges over [0, log n] and the paper itself reports H=2.87 in Section 4.1. The PELTS state space and label alphabet therefore exclude the very values the monitor is required to process. Replace R[0,1] by R_{\\ge 0} throughout the formal definitions, or explicitly introduce and apply a normalization step.","section":"Definitions 4.4 and 4.5"},{"comment":"The TDA pipeline is under-specified. The text states that persistent homology was computed with jHoles using the weighted rank clique homology algorithm, but it does not specify the filtration thresholds, the weighting scheme used to turn the coexistence matrix into a filtered simplicial complex, how the β0 and β1 barcodes are combined into the PE values, or how the 'average sequence' in Figure 4 is computed over simulations. These details are necessary to reproduce the PETs and to assess whether the two plateaus are robust features rather than artifacts of smoothing or parameter choice.","section":"Section 4.1"}],"minor_comments":[{"comment":"Section 3.2 states that 'several (in the order of hundreds) simulations' were executed, while Section 5.1 reports 1000 simulations; please align the two numbers.","section":"Section 3.2"},{"comment":"The word 'typycally' before the discussion of state-based traces should be corrected to 'typically'.","section":"Section 4"},{"comment":"The caption says 'PE of IS computed from a simulation', but the surrounding text describes the average sequence of PE values; clarify which quantity is actually plotted.","section":"Figure 4"},{"comment":"Definition 4.7 uses abbreviated path notation such as ((·,·,ϵ))+ without defining the shorthand; please expand the notation or add a sentence explaining the regular-expression-like operators.","section":"Definition 4.7"},{"comment":"The bounded-LTL formulas use symbols like 2≤30 and © without a semantics table; since the paper targets runtime verification, define the bounded operators and the next operator for finite traces.","section":"Section 5.1"}],"recommendation":"major_revision","confidential_remarks":"The paper appears to be a condensed account of prior thesis and workshop work; the genuinely new element is the PELTS semantics and MPEA trace formulation, which is a useful formalization. However, the empirical section does not validate the central claim, and the formal definitions contain a codomain error for PE values. I would encourage the editor to require the authors to either add a proper validation study or substantially weaken the abstract's claim, because as written the contribution is a formal framework with an unverified illustrative case study."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The useful part of this paper is the formal semantics. The PELTS operational rules in Definition 4.5 are coherent, and the MPEA extension with atomic propositions is a legitimate step that gives the earlier PEA construction a proper run-time verification interface. If the paper were read narrowly as a formal framework, it would be acceptable and even a reasonable starting point for further work.\n\nThe problem is the empirical claim in the abstract: that applying the monitor to simulated traces reveals temporal properties that should hold for reaching immunization memory. That claim is not backed by what is shown. The steady states in Section 4.1 are fixed by hand from a smoothed PE plot, with H=0 and H>0 conditions assigned by inspection. The memory self-loop is added from the shape of the second peak, and the virgin self-loop is added from domain knowledge even though the authors say it was not observed. That is not necessarily fatal, but it means the 198/780/22 trace classification in Section 5.1 inherits all of those hand-set choices. No independent indicator of immune memory (like memory-cell counts or secondary-response success) is compared against the MPEA verdicts, so there is no ground truth. The three bounded-LTL formulas are presented as examples that could be checked, not as invariants mined from the 1000 traces with any statistical support. The word \"reveals\" in the abstract oversells what the paper actually demonstrates.\n\nI want to be fair: the paper does not hide these limitations. The text explicitly says the self-loop was not observed and that the properties are examples. The definitions are clearly written and the citations are appropriate. The main issue is that the central advertised result is feasibility, and the feasibility evidence is too thin. The formal part deserves to be published, but not with the current empirical framing.\n\nI would still send this to peer review. A good referee can separate the salvageable formal core from the unsupported empirical interpretation, and the PELTS semantics is a real contribution that should be available to the community. I would not cite it for the monitoring results, but I might cite it for the PELTS definitions.","headline":"The formal PELTS/MPEA semantics is clean and worth preserving, but the paper's central empirical claim about immunization memory is not supported by the reported evidence.","tokens_in":16266,"tokens_out":941,"would_cite":false,"duration_ms":11531,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims that plateaus in persistent entropy mined from component-level data can be turned into an automaton whose traces separate immune-memory successes from failures and yield bounded temporal-logic invariants.","keywords":["runtime verification","persistent entropy","topological data analysis","persistent homology","self-adaptive systems","bounded LTL","specification mining","immune system simulation"],"falsifier":"Run the MPEA on a simulation with no antigen injection: if the persistent-entropy series ever shows a plateau with $H>0$ and $\\dot H=0$, the monitor labels a never-immunized system as memory, falsifying the claimed invariant. Alternatively, delete the unobserved virgin self-loop and check whether any trace of the form $\\{virgin\\}^{+}\\{\\omega\\}^{+}\\{virgin\\}^{+}$ survives.","tokens_in":15260,"feed_emoji":"🧬","tokens_out":10737,"duration_ms":100562,"temperature":0.7,"pith_summary":"This paper proposes a way to turn streamed observations of a complex system into a small automaton that can be run against execution traces to detect whether the system is behaving as it should. The construction is data-driven: from each time sample the authors compute a topological summary—persistent entropy, a single number measuring how ordered the system's connectivity structure is—and mine steady states from plateaus in that series. Those steady states become the locations of a Persistent Entropy Automaton, and a labeled-transition-system semantics turns any trace into a word over atomic propositions and transition symbols. Applied to 1000 simulated immune-system runs, the monitor separates traces ending in a memory state from traces that never reach immunization, and yields bounded temporal-logic properties that successful runs satisfy. If the construction is sound, any complex system whose components produce observable interaction data can be monitored without a global model.","feed_headline":"A topology-mined automaton separates immune-memory from failed runs","feed_subtitle":"Persistent entropy builds an automaton that separates traces ending in immune memory from those that fail to immunize.","key_machinery":"The load-bearing object is the Persistent Entropy Automaton (PEA). Persistent entropy $H(t)$ is the Shannon entropy of the lengths of the bars in a persistence barcode; the PEA's states are equilibrium conditions expressed as boolean combinations of $H$ and its discrete derivative $\\dot H$. The associated PELTS determines when the system stays in a steady state (Steady), leaves it (StartT), travels through intermediate observations (ContT), and settles into a next steady state (StopT). The Monitor PEA adds atomic propositions to steady states, so each execution yields a trace over $\\{\\text{virgin},\\text{memory},\\omega\\}$, with $\\omega$ marking the non-instantaneous transition phases; these traces are the objects on which bounded LTL formulas are evaluated.","core_discovery":"The central claim is that a Persistent Entropy Automaton, augmented with atomic propositions into a Monitor PEA (MPEA), can act as a run-time monitor mined entirely from component-level data. The paper formalizes the PEA by defining its semantics as a persistent entropy labelled transition system (PELTS) with four rules—steady, start transition, continue transition, stop transition—so that a time series of persistent entropy values induces a set of executions. On the Idiotypic Network case study, running 1000 simulated traces through the MPEA classifies 198 traces as ending in virgin, 780 as ending in memory, and 22 as ending inside a transition; the final class is read as a violation. From these trace classes the paper derives bounded LTL properties, such as 'an immunization phase that starts ends within 180 ticks,' that must hold if the system is to reach immunization memory.","pith_inferences":["A natural next step the paper leaves open is online monitoring: because the PELTS marks transition phases with $\\omega$, an alarm could be raised the moment a trace enters $\\omega$ and stays there beyond the 180-tick bound used in the mined properties, rather than only after the trace ends.","The reported trace counts (780 successes against 22 violations out of 1000) imply the monitor could be calibrated as a probabilistic statement about simulator configurations—for instance, how large the antibody repertoire must be—but the paper does not run that statistical analysis.","If the equilibrium conditions were replaced by a statistical rule for plateau detection, the entire pipeline would become parameter-free; that would let the method transfer to other streams (network traffic, sensor logs) without case-by-case human judgment.","The paper does not report a negative control; shuffling the time order of persistent entropy values and re-deriving the PEA would test whether the virgin/memory split is an artifact of the smoothing."],"forward_implications":["The same pipeline—coexistence matrix, persistent homology, persistent entropy, plateau extraction—produces a monitor for any time-evolving weighted graph, not only immune-system simulations.","Trace classes give an operational meaning to 'immunization memory': a run reaches memory exactly when the MPEA trace ends in $\\{memory\\}$, and the 22 traces ending in $\\{\\omega\\}$ are detectable failures (insufficient antibody repertoire or too-short simulation).","The mined properties become checkable obligations: for example, every started immunization phase must end within 180 ticks, a bounded temporal-logic formula over the MPEA trace alphabet.","Because the MPEA is derived from data rather than from a hand-written model, it can be re-derived whenever the system changes, giving a run-time verification layer for self-adaptive systems."],"supporting_citations":[{"why":"Introduces the data-driven PEA derivation methodology that this paper formalizes and extends with equilibrium conditions and semantics.","marker":"[33]"},{"why":"Defines persistent entropy, the scalar observable from which the automaton states are mined.","marker":"[44]"},{"why":"Supplies the clique-weight rank persistent homology implementation used to compute the persistence barcodes and PE values for the case study.","marker":"[5]"},{"why":"Describes the online immune-system simulator used to generate the 1000 simulated traces analyzed by the monitor.","marker":"[41]"},{"why":"Provides the bounded LTL semantics used to express the mined temporal invariants.","marker":"[24]"},{"why":"Supplies the runtime-verification background that motivates turning an automaton into a monitor with verdicts on finite traces.","marker":"[26]"}],"fun_headline_variants":["Persistent entropy automaton spots immune memory in real time","Topology-built monitor learns immune system's memory rules","Data-mined automaton flags failed immune runs instantly","Run-time watch from component data predicts immune outcome"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Everything hangs on the manually chosen equilibrium conditions—virgin is $H=0$ with $\\dot H=0$, memory is $H>0$ with $\\dot H=0$—read by eye from a smoothed persistent-entropy plot, together with automaton structure (a memory self-loop suggested by the two-peak shape and a virgin self-loop imported from biological knowledge though never observed).","fun_headline_variants_meta":{"raw":{"variants":["Persistent entropy automaton spots immune memory in real time","Topology-built monitor learns immune system's memory rules","Data-mined automaton flags failed immune runs instantly","Run-time watch from component data predicts immune outcome"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000252,"raw_usage":{"total_tokens":1541,"prompt_tokens":909,"completion_tokens":632,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":525,"completion_tokens_details":{"reasoning_tokens":569}},"tokens_in":525,"tokens_out":632,"duration_ms":16503,"temperature":1.0,"reasoning_tokens":569,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:55:51.828164+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the MPEA on a simulation with no antigen injection: if the persistent-entropy series ever shows a plateau with $H>0$ and $\\dot H=0$, the monitor labels a never-immunized system as memory, falsifying the claimed invariant. Alternatively, delete the unobserved virgin self-loop and check whether any trace of the form $\\{virgin\\}^{+}\\{\\omega\\}^{+}\\{virgin\\}^{+}$ survives.","supporting_citations":[{"cited_title":"Topological characterization of complex systems: Using persistent entropy.Entropy, 17(10):6872–6892, 2015","cited_arxiv_id":null,"evidence_quote":"Introduces the data-driven PEA derivation methodology that this paper formalizes and extends with equilibrium conditions and semantics."},{"cited_title":"Characterisation of the idiotypic immune network through persistent entropy","cited_arxiv_id":null,"evidence_quote":"Defines persistent entropy, the scalar observable from which the automaton states are mined."},{"cited_title":"jHoles: A Tool for Understanding Biological Complex Networks via Clique Weight Rank Persistent Homology.Electronic Notes in Theoretical Computer Science, 306:5–18, 2014","cited_arxiv_id":null,"evidence_quote":"Supplies the clique-weight rank persistent homology implementation used to compute the persistence barcodes and PE values for the case study."},{"cited_title":"Immune system simula- tion online","cited_arxiv_id":null,"evidence_quote":"Describes the online immune-system simulator used to generate the 1000 simulated traces analyzed by the monitor."},{"cited_title":"Simple Bounded LTL Model Checking","cited_arxiv_id":null,"evidence_quote":"Provides the bounded LTL semantics used to express the mined temporal invariants."},{"cited_title":"A brief account of runtime verification.The Journal of Logic and Algebraic Programming, 78(5):293– 303, 2009","cited_arxiv_id":null,"evidence_quote":"Supplies the runtime-verification background that motivates turning an automaton into a monitor with verdicts on finite traces."}],"review_version":1}