{"id":"f6891283-8be8-49b8-a65e-90021277f63a","arxiv_id":"2509.05596","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"An approach that verifies behavioral containment between old and new versions of PLC software by translating Sequential Function Charts into Petri nets and comparing symbolic execution paths.","lead":"This paper checks that upgraded factory control software still does what the old version did by comparing mathematical models of both versions. It reports a roughly 4x speedup over an existing tool on 80 programs from an open-source library.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 2's soundness rests on an unproved path-cover completeness premise: nothing shows Algorithm 3 always yields a finite path cover satisfying Definition 9 for SFC-derived Petri nets.","rationale":"The reader's weakest assumption identifies exactly the gap I find most load-bearing: the soundness theorem assumes a property that the paper motivates with one example but never proves. The paper's own limitations reinforce the concern: Section 9 explicitly limits the approach to loops traversed exactly once, and Section 7.2 demonstrates a functionally equivalent SFC for which the path construction cannot establish containment. Those passages are evidence that path-cover completeness is not automatic for the supported fragment. I did not find a stronger or more fundamental defect: the algorithm's structure is plausible, the running example is coherent, and conditional on a genuine path cover the proof strategy of Theorem 2 is reasonable. The correct disposition remains conditional acceptance pending either a completeness proof for the path-cover construction or an explicit characterization of the subclass of SFC-derived Petri nets for which the construction is complete, together with a reproducible benchmark artifact. Because the reader already recommended CONDITIONAL, my stress-test does not move the verdict.","tokens_in":23735,"tokens_out":6282,"duration_ms":63358,"concrete_test":"Run a small-scale completeness check: implement the SFC-to-Petri-net translation and Algorithms 2 and 3 from the paper, then for a minimal net with a loop containing two parallelizable transitions (and for the Figure 5 example) enumerate all reachable out-port computations up to four ticks under Definition 3. For each enumerated computation, test whether it can be written as a sequence of parallel compositions of paths from the generated path set Π'. If any computation is not expressible, the path-cover premise of Theorem 2 is false for that net, so an empty Πn,0 would not imply containment.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central soundness claim, Theorem 2, is conditional on the assumption that the path set Π0 produced by Algorithm 3 is a path cover of N0 in the sense of Definition 9. Both Theorem 1 and the proof of Theorem 2 begin by asserting 'Since Π0 gives a path cover of N0', but no theorem establishes that the static plus execution cut-points of Definition 8 always decompose every computation of an out-port into a finite concatenation of parallelizable paths. Example 2 motivates execution cut-points on one manually chosen net, and Definition 9 only defines what a path cover is; it does not prove that Algorithm 3's construction achieves one. The paper's own Section 9 restricts the method to traversing each loop exactly once, and Section 7.2 shows a functionally equivalent but non-bisimilar SFC whose loop splitting defeats the path construction. If some reachable computation of N0 cannot be expressed with the generated path set, then Algorithm 1 can return Πn,0 = ∅ while silently omitting that computation; the reported 'N0 ⊑ N1' would be a false positive, contradicting the Section 9 claim that the tool 'does not give any false positive results'. This unproved path-cover completeness is the load-bearing gap: it is exactly the step that turns syntactic path matching into a guarantee about all computations.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a verification approach for PLC software upgrades. SFC programs from an old and a new version are translated into deterministic, 1-safe Petri net models with tick-labeled transitions, and the new model is checked for containment of the old model via symbolic path equivalence. The central theorems (Theorem 1 and Theorem 2) claim that if the algorithm finishes with no unmatched paths in the old model, containment holds. The approach is evaluated on 80 OSCAT-based benchmarks grouped into four classes, with a reported roughly 4x speedup over verifAPS. The paper also reports fault-injection experiments and discusses limitations including non-bisimilar functionally equivalent SFCs and the restriction to traversing loops exactly once.","tokens_in":24064,"tokens_out":4615,"duration_ms":44990,"significance":"If the soundness claim were fully established, the paper would offer a useful, scalable regression-verification tool for a restricted but industrially relevant class of SFC upgrades: the translation to Petri nets is syntactic and simple, the tick-aware execution cut-points are a sensible adaptation to synchronous PLC semantics, and the symbolic path-based checker has the potential to avoid state-space explosion. The 80-benchmark OSCAT evaluation and the explicit comparison with verifAPS are also valuable empirical contributions. However, the significance is conditional: the central soundness theorem rests on an unproved path-cover completeness premise, and the evaluation is reported only as aggregate numbers for four classes without an artifact or per-benchmark data. The paper does not ship machine-checked proofs or reproducible code, and the core path-equivalence machinery is largely imported from the authors' prior work [1,2], which limits independent verification.","major_comments":[{"comment":"The soundness of the containment checker is conditional on an unproved premise: the proof of Theorem 2 in the Appendix begins by asserting 'Let Π0 gives a path cover of N0', but no theorem establishes that the paths generated by Algorithm 3 always form a path cover in the sense of Definition 9 for the supported subclass of SFC-derived Petri nets. Example 2 merely shows insufficiency of static cut-points; Section 7.2 and Section 9 admit that loops are traversed exactly once and that a functionally equivalent but non-bisimilar SFC defeats the path construction. If some reachable computation of an out-port in N0 cannot be expressed as a finite concatenation of parallelizable paths from the generated Π0, then Algorithm 1 can return Πn,0 = ∅ while silently omitting that computation. The reported 'N0 ⊑ N1' would then be a false positive, contradicting the Section 9 claim that the method 'does not give any false positive results.' The authors must either prove path-cover completeness for the supported subclass, or explicitly restrict Theorem 2 and the no-false-positive claim to models for which the generated path set is a complete path cover.","section":"§5, Theorem 2; Appendix, Algorithms 2-3; Definition 9"},{"comment":"The treatment of 'uncommon variables' can itself introduce false positives. Step 8 removes all uncommon variables and then computes Rβ and rβ, and Definition 10(4) allows arbitrary association of removed variables with newly introduced variables via ηv. In the running example, the new safety-guard variable S is dropped from the execution condition of path β1·β2, so path equivalence is claimed even though the new guard can, when false, block the old behavior (the robot remains immobilized). No side condition is given to ensure that along every corresponding path the newly introduced guard is always enabled. Without such an invariant, dropping a new guard that affects control flow can make Rα ≡ Rβ even when the old computation has no counterpart in N1. This is a second, independent route to the false positives that Section 9 rules out, and it needs an explicit justification or a restriction on when uncommon-variable elimination is sound.","section":"§5, Algorithm 1 step 8; Definition 10(4)"},{"comment":"The experimental claims are not supported by the data as reported. Table 2 aggregates results into four classes ('Basic', 'Simple', 'Medium', 'Complex') rather than reporting the 80 individual benchmarks, and it gives no standard deviations, per-benchmark path counts, or timings. The 'nearly 4x' comparison with verifAPS is therefore not substantiated beyond four average points. Table 3 reports a '–' for the Type 2 verifAPS time without explaining whether the tool timed out, crashed, or was not run; this is essential for judging the claim that Type 2 cannot be detected by verifAPS. The paper also provides no artifact, no per-benchmark data, and no independent ground truth for the equivalence labels, making it impossible to check whether the tool's 'yes' and 'no' answers are correct. I recommend providing the benchmark set, the tool, or at least a detailed per-benchmark table with error bars, and a clear protocol for the fault-injection ground truth.","section":"§6, Tables 2 and 3"}],"minor_comments":[{"comment":"The statement of Theorem 2 in the Appendix is truncated: it reads 'returns Πn,0' with no completion of the condition, while the main-text version is complete. This should be fixed.","section":"Appendix, Theorem 2 statement"},{"comment":"Some figure references are inconsistent: Section 2 refers to 'Figure 3(a)' and 'Figure 4(c)' where the surrounding text about the original SFC and its Petri net is not always aligned with the captions, and Section 3 references 'Figure 1' for the functional block diagram that appears as Figure 2.","section":"§2 and §4, figure references"},{"comment":"The sentence 'The method is not scalable at all' is vague and contradicts the scaling claims of Section 6; if the authors mean the method does not scale to non-bisimilar or hierarchical SFCs, that should be stated precisely rather than as a blanket scalability claim.","section":"§7.2"},{"comment":"Notation is inconsistent: equivalence of computations is written ≃c, equivalence of models is written ≃ (Definition 7), and path equivalence is written ≃ (Definition 10); the subscripts are dropped in places, making it hard to distinguish computation equivalence from path equivalence. A small notation table would help.","section":"Definitions 5-7 and 11"},{"comment":"The phrase 'one token corresponds to k variables' in the 1-safe discussion is unclear, and the sentence 'Our Petri net model is deterministic and 1-safe' is asserted without proof; since determinism is used in Definition 4, it should be justified from the SFC translation rules.","section":"§4, Definition 2, text after Definition 2"}],"recommendation":"major_revision","confidential_remarks":"The paper's central novelty is modest relative to the authors' prior work [1,2], and the absence of an artifact makes independent verification difficult. The most serious issue is not a typo or a missing experiment but the unproved path-cover completeness premise in Theorem 2 and the unsound-looking uncommon-variable elimination; both can in principle be repaired by adding proofs or by weakening the no-false-positive claim to a conditional statement. If the authors cannot supply the missing proof or a clear restriction on the supported subclass, the soundness claim should not be published in its current form. I would not reject outright, because the practical setting and the tick-aware execution cut-points are promising, and a revised version with a precise completeness statement and a reproducible evaluation could be acceptable."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Straight to the point: this paper is a plausible, incremental engineering contribution that deserves a serious referee, but its central soundness claim is not actually proved. The authors adapt their earlier path-based Petri net equivalence work to SFC programs, add tick-aware execution cut-points, and propose path extension/merging heuristics. On 80 OSCAT benchmarks they report roughly 4x speedup over verifAPS. The running example is clear, and to their credit they are explicit that the tool is incomplete and fails on functionally equivalent but non-bisimilar programs (Section 7.2).\n\nThe serious problem is exactly the one the stress-test note identifies. Theorem 2 and Theorem 1 both assume 'Π0 gives a path cover of N0,' but nothing shows that Algorithm 3 always builds a path cover satisfying Definition 9. Definition 9 only defines what a path cover is. Example 2 motivates extra cut-points on one manually chosen net, yet there is no general argument that the static-plus-execution cut-point construction covers every computation of an out-port for the supported SFC-derived Petri nets. The paper's own restriction—each loop traversed exactly once—makes the assumption even less safe. Since a 'contained' answer is checked only against the generated paths, an unrepresented computation could be silently missed. So the Section 9 claim 'does not give any false positive results' is not supported by the paper's theorems. This is a load-bearing gap, not a stylistic nitpick.\n\nThe evaluation is also weaker than the text implies. No code or benchmark artifacts are shipped, there is only one average time per benchmark class, no variance or repetitions are reported, and the verifAPS comparison is a single table. The controlled field trial mentioned in Section 7.1 is a ballpark claim with no protocol; I would not cite it.\n\nWhat is genuinely good: the SFC-specific modeling choices (action sequences per place, guard-only transitions, tick semantics) are a reasonable refinement of earlier work, and the path extension/merging ideas are clearly motivated by the running example. Self-citation of the path equivalence machinery is not itself a flaw. The problem is that the completeness property on which soundness rests is assumed, not proven.\n\nThis paper is for researchers and tool builders in PLC/automation verification who want a fast symbolic regression check within a clearly delimited fragment. I would send it to peer review, not desk reject, but ask for (a) a proof of path-cover completeness, or a precise fragment in which it provably holds, and (b) a reproducible evaluation. I would not cite it in its current form. Reading group: maybe, because the gap is a good teaching point.","headline":"Plausible SFC regression-checking tool with a real speed claim, but the soundness proof quietly assumes the path-cover completeness that is never proven.","tokens_in":24490,"tokens_out":4511,"would_cite":false,"duration_ms":38254,"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 a containment checker on Petri nets derived from Sequential Function Charts can soundly verify that an upgraded PLC program preserves every behavior of the original, and that it runs about four times faster than…","keywords":["PLC software verification","Sequential Function Chart (SFC)","Petri net containment","symbolic path equivalence","execution cut-points","software evolution","regression verification","model checking"],"falsifier":"Construct an original and an upgraded SFC that are behaviorally different only on a second traversal of a loop, for example a guard inside the loop that becomes true only after the first iteration, so that the path cover, which visits each loop exactly once, collapses both iterations into a single path. If the checker reports containment on such a pair, the soundness claim of Theorem 2 is falsified because a computation with different behavior on the second traversal would have been missed.","tokens_in":1570,"feed_emoji":"⚙️","tokens_out":2362,"duration_ms":65225,"temperature":0.7,"pith_summary":"The paper tries to prove that when PLC software is upgraded, the new version still performs every behavior the old version performed. It translates both versions of a Sequential Function Chart into Petri nets and runs a containment check based on symbolic path equivalence, using execution cut-points that respect PLC tick semantics. If the check succeeds, the old model is contained in the new model, meaning every computation of the old program has an equivalent computation in the upgrade. The paper proves this containment check is sound, meaning it reports no false positives, and measures roughly a fourfold speedup over the verifAPS tool on 80 OSCAT benchmarks. A sympathetic reader cares because regression testing of PLC code is slow and incomplete, and this offers a formal, automated check that a safe upgrade has not silently broken existing functionality.","feed_headline":"Containment checker verifies PLC upgrades 4x faster","feed_subtitle":"It converts both SFC versions to Petri nets and checks that every old computation exists in the new one.","key_machinery":"The engine is the execution cut-point: a place in the Petri net that is either a static cut-point (initial marking, branch point, back-edge root, or out-port) or is marked during tick-tracking execution when a parallel thread is created. Cut-points split the net into a finite set of paths, and the path cover is the set of all such paths. Containment is checked by comparing each old path against candidate new paths through a normalization step, the WFF constructor, which checks equivalence of the execution-condition formula and the data-transformation expression, with path extension and path merging applied when a candidate path is too short or must be stitched together with converging paths. Tick stamps on the last transitions of matched paths align PLC ticks between the two models.","core_discovery":"The central claim is Theorem 2: if the containment checker algorithm terminates with the set of unmatched old-model paths, $\\Pi_{n,0}$, empty, then the old Petri net model $N_0$ is contained in the new model $N_1$, written $N_0\\sqsubseteq N_1$. Containment means that for every out-port $p$ of $N_0$ and every computation $\\mu_p$ of $p$, there is a computation $\\mu_{p'}$ of the corresponding out-port $p'=f_{\\mathrm{out}}(p)$ of $N_1$ such that the two computations have equivalent execution conditions and identical data transformations. The proof works through a path-cover argument: any computation of $N_0$ can be decomposed into a finite sequence of concatenations of parallelizable paths from the constructed path cover, and each such path is matched, possibly after extension or merging, to an equivalent path of $N_1$. The paper also reports that on 80 OSCAT benchmarks the containment check takes 1.43 to 6.12 seconds, about four times faster than verifAPS, and that faulty upgrades are detected with similar speed.","pith_inferences":["A natural next step is to make the path-cover construction itself the object of proof or empirical validation: on small SFCs, one could compare the constructed path cover against the full reachability graph of the Petri net to measure coverage, something the paper does not do.","The directionality of containment is well matched to software evolution: an upgrade that only adds new behavior, such as a safety interlock, is contained in the reverse direction, and the tool's asymmetric verdicts correspond to this practical asymmetry.","The reported BisimDegree, the ratio of matched paths to total paths, could serve as a regression-risk score for partial upgrades, letting engineers prioritize manual review of unmatched paths rather than discarding the whole verification.","The tick-alignment mechanism, devised for PLCs, may transfer to other tick-based reactive languages such as synchronous dataflow languages, where path-based equivalence has not yet been applied."],"forward_implications":["A passing containment check means the upgraded PLC code preserves every old out-port computation, so the preserved portion needs no further regression testing.","Because the SFC-to-Petri-net translation is syntactic, the approach extends to any control program that can be mapped to a Petri net, independent of the original PLC language.","On the 80 OSCAT benchmarks, containment checking completes in 1.43 to 6.12 seconds, roughly four times faster than verifAPS, and faulty upgrades are detected in similar time.","The report generator lists matched and unmatched paths, so a failed check pinpoints concrete places where the upgrade diverges from the original.","The tool is sound but not complete: a behavior-preserving but non-bisimilar upgrade may be reported as non-containment, requiring manual review."],"supporting_citations":[{"why":"Supplies the static and dynamic cut-point framework and the path-equivalence checking on which the containment checker builds.","marker":"[1]"},{"why":"Defines parallelizable paths and the earlier path construction algorithm that execution cut-points extend.","marker":"[2]"},{"why":"Is the verifAPS tool and method (SFC to Structured Text to SMV with inductive equivalence checking) that the experiments compare against and report roughly a fourfold speedup over.","marker":"[5]"},{"why":"Provides the unifying SFC semantics that justifies translating Sequential Function Charts into Petri nets.","marker":"[6]"},{"why":"Supplies the normalized-form theorem prover, the WFF constructor, used to check equivalence of execution conditions and data transformations.","marker":"[8]"}],"fun_headline_variants":["PLC upgrade safety: containment check cuts verification time 4x","Model containment approach verifies PLC upgrades 4x faster","4x faster verification of PLC upgrades via model containment","Containment-based PLC upgrade verifier outperforms verifAPS","Symbolic path equivalence speeds PLC upgrade verification 4x"],"cache_read_input_tokens":26624,"weakest_assumption_plain":"The argument assumes that the set of paths the constructive algorithm generates is a genuine path cover: every computation of the old model can be written as a finite concatenation of parallelizable paths from that set, even though each loop is traversed exactly once and the paper does not prove that the constructive path generation always yields such a cover.","fun_headline_variants_meta":{"raw":{"variants":["PLC upgrade safety: containment check cuts verification time 4x","Model containment approach verifies PLC upgrades 4x faster","4x faster verification of PLC upgrades via model containment","Containment-based PLC upgrade verifier outperforms verifAPS","Symbolic path equivalence speeds PLC upgrade verification 4x"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000549,"raw_usage":{"total_tokens":2614,"prompt_tokens":933,"completion_tokens":1681,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":549,"completion_tokens_details":{"reasoning_tokens":1598}},"tokens_in":549,"tokens_out":1681,"duration_ms":11529,"temperature":1.0,"reasoning_tokens":1598,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T16:20:47.983691+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct an original and an upgraded SFC that are behaviorally different only on a second traversal of a loop, for example a guard inside the loop that becomes true only after the first iteration, so that the path cover, which visits each loop exactly once, collapses both iterations into a single path. If the checker reports containment on such a pair, the soundness claim of Theorem 2 is falsified because a computation with different behavior on the second traversal would have been missed.","supporting_citations":[{"cited_title":"Equiva- lence checking of petri net models of programs using static and dynamic cut-points","cited_arxiv_id":null,"evidence_quote":"Supplies the static and dynamic cut-point framework and the path-equivalence checking on which the containment checker builds."},{"cited_title":"Mandal, Kunal Banerjee, and Krishnam Raju Duddu","cited_arxiv_id":null,"evidence_quote":"Defines parallelizable paths and the earlier path construction algorithm that execution cut-points extend."},{"cited_title":"Proving equivalence between control software variants for pro- grammable logic controllers","cited_arxiv_id":null,"evidence_quote":"Is the verifAPS tool and method (SFC to Structured Text to SMV with inductive equivalence checking) that the experiments compare against and report roughly a fourfold speedup over."},{"cited_title":"A unifying semantics for sequential function charts","cited_arxiv_id":null,"evidence_quote":"Provides the unifying SFC semantics that justifies translating Sequential Function Charts into Petri nets."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the normalized-form theorem prover, the WFF constructor, used to check equivalence of execution conditions and data transformations."}],"review_version":2}