{"id":"1201ef0e-b699-4c9e-ab15-2a97e5f11f42","arxiv_id":"2608.10254","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"high","formal_verification":"none","parameter_count":3,"one_line_summary":"This paper is a tutorial on building conservative discrete abstractions for verification of cyber-physical systems, but its proposed self-loop erasure technique can under-approximate the true one-step transitions.","lead":"This tutorial offers a four-step recipe for turning a continuous control system into a finite-state model that can be checked with symbolic model checking, and it tests the recipe on three case studies. Engineers get a clear structure for building conservative abstractions, but the self-loop erasure step is not sound as written, so the central conservative-by-construction guarantee fails.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Self-loop erasure in §7 is unsound: certifying exit within K>1 steps does not justify deleting the self-loop, so Definition 3 condition 3 can fail and the abstraction can under-approximate the concrete dynamics.","rationale":"The reader's weakest assumption is exactly the load-bearing flaw I find. Definition 3's condition 3 is a per-step inclusion, not a finite-horizon inclusion. A finite-time escape certificate with K>1 only rules out trajectories that stay in the cell for K consecutive steps; it does not rule out single-step transitions that remain inside the cell. Since the self-loop is the only transition that can cover such one-step images, erasing it creates an under-approximation. The paper's own running example uses K=10, and Tables 2 and 3 report applying this erasure widely, so the flaw is not incidental. Other issues, such as Algorithm 2's 'Post ← Post ∩ {x′}' typo and the PAC sampling guarantee covering only β-significant transitions, are real but secondary; the self-loop erasure directly breaks the claimed conservative-by-construction invariant. The flaw is localized and repairable, but as submitted the central claim does not hold, so REJECT is the appropriate verdict for this version.","tokens_in":21748,"tokens_out":8864,"duration_ms":96380,"concrete_test":"Use the one-dimensional partition C=[0,1), D=[1,2) and define f(x)=x+0.6. For x∈[0,0.4), f(x)∈C and f²(x)∉C; for x∈[0.4,1), f(x)∉C, so every trajectory exits C within K=2 steps and §7 would erase the self-loop C→C. Build Post(C)={C,D}, erase the self-loop, and check Definition 3 condition 3 at x=0.1: f(0.1)=0.7∈C, but C is no longer in Post(C), so the required inclusion fails. This settles that the erasure criterion is insufficient; repair by requiring one-step escape (R₁=∅) or by splitting the cell so that every one-step image is covered.","verdict_should_be":"REJECT","load_bearing_attack":"Section 7 ('Assured self-loop erasure') claims that if every concrete trajectory originating in Ψ(x̂) exits within K steps, the self-loop (x̂, σ, x̂) may be purged. This is incompatible with Definition 3 condition 3, which requires for every x̂ that f(Ψ(x̂)) ⊆ ∪_{x̂′ ∈ Post(x̂)} Ψ(x̂′). The self-loop is the only element of Post(x̂) covering one-step images that remain inside the cell. Certifying exit within K steps with K>1 still permits states x ∈ Ψ(x̂) with f(x) ∈ Ψ(x̂); the trajectory simply leaves on a later step. Deleting the self-loop removes exactly the transition needed to represent those one-step behaviors. The paper's own reachable-set propagation (Eq. 13) illustrates the problem: R₁ = Ψ(x̂) ∩ AABB(f(Ψ(x̂))) can be nonempty while R_K = ∅; the certificate proves R_K empty, not R₁ empty. The running example uses K=10, so this is not an edge case. After erasure, condition 3 fails, the abstraction under-approximates the concrete system, and the implication ŝ ⊨ φ̂ ⇒ s ⊨ φ no longer follows. Because Step 3 is applied in every case study and the paper's headline claim is 'conservative-by-construction', this unsound erasure is a load-bearing flaw in the central claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a four-step workflow for building finite-state abstractions of deterministic discrete-time cyber-physical systems such that abstract satisfaction of a lifted LTL property implies concrete satisfaction. Step 1 partitions the state space into a rectilinear grid; Step 2 constructs conservative transition relations using axis-aligned bounding boxes, polytopes, or sampling with PAC-style coverage certificates; Step 3 removes self-loops and spurious transitions via certified erasure and counterexample-guided abstraction refinement; Step 4 lifts the LTL specification using may/must semantics. The workflow is demonstrated on three case studies, reporting abstraction metrics, verification times, and true-positive rates. The central claim is that the pipeline is conservative-by-construction and therefore sound for model checking.","tokens_in":22001,"tokens_out":12610,"duration_ms":125982,"significance":"If the soundness claim were correct, this would be a useful tutorial consolidating standard abstraction techniques and offering practical guidance on common pitfalls. The paper is clearly written and gives credit to prior work; it also ships code, uses standard PAC missing-mass bounds, and evaluates the pipeline on three systems with a reference reachability computation. However, the load-bearing soundness argument for self-loop erasure is incorrect, and the sampling-based methods do not produce abstractions that are conservative in the sense of Definition 3. These issues affect the headline conservatism claim and the interpretation of the experimental results, so a substantial revision is needed before the paper can be accepted.","major_comments":[{"comment":"The criterion that every concrete trajectory originating in Psi(x-hat) exits the cell within K steps does not justify deleting the self-loop (x-hat, sigma, x-hat). Definition 3, condition 2, requires the one-step image f(Psi(x-hat)) to be covered by the successors of x-hat, and a trajectory can remain inside Psi(x-hat) for k < K steps before exiting. The propagation R_{k+1} = R_k intersect AABB(f(R_k)) can have R_1 nonempty while R_K is empty; the certificate proves only that no trajectory survives K steps, not that no state has its one-step image inside the cell. Since the running example uses K=10 and the erasure is applied in all case studies (Tables 2 and 3), the resulting abstraction can under-approximate the concrete dynamics and the implication s-hat models phi-hat => s models phi no longer follows. The erasure criterion should be one-step escape (K=1) or the abstraction must be augmented with additional states or transitions that preserve the intermediate one-step behavior.","section":"Section 7, 'Assured self-loop erasure', Eq. (13)"},{"comment":"The sample-based erasure certificate is even weaker than the deterministic one. If all N K-length rollouts exit, Eq. (14) only establishes q_tau >= gamma^{1/N} with confidence 1-gamma; it does not establish q_tau = 1. For the running-example parameters (N=100, gamma=0.1), the certified lower bound is only 0.79. Moreover, even a certificate that every trajectory exits within K steps does not rule out one-step images staying in the cell, so deleting the self-loop remains unsound for the same reason as the deterministic erasure. Removing self-loops under this certificate can therefore remove genuine transitions and violate Definition 3.","section":"Section 7, 'Sampling-based with PAC guarantee', Eq. (14)"},{"comment":"The sampling-based transition construction does not produce a conservative abstraction in the sense of Definition 3. The PAC missing-mass certificate guarantees only that all transitions with category probability at least beta under Unif(X) are observed, whereas condition 2 of Definition 3 is universal over x in X and includes transitions from measure-zero sets. Thus an abstraction built by Algorithm 4 can verify a property while a rare concrete trajectory violates it. The abstract's 'conservative-by-construction' claim should be restricted to the AABB and polytope methods, or the paper should explicitly frame sampling as a probabilistic verification method with a residual risk.","section":"Section 6.3, Algorithm 4 and Eq. (11)"},{"comment":"The update 'Post_s <- Post_s intersect {x-hat-prime}' should be a union; as printed, the intersection with a singleton either leaves Post_s empty or, if Post_s is nonempty, deletes all previously added successors. Consequently, GetSuccessorsAABB as written always returns the empty set and cannot satisfy condition 2 of Definition 3. Please correct this to 'Post_s <- Post_s union {x-hat-prime}'.","section":"Section 6, Algorithm 2, line 5"}],"minor_comments":[{"comment":"The text refers to 'Condition 3' but only two conditions are enumerated; the transition condition is condition 2.","section":"Section 3.2, Definition 3"},{"comment":"The antecedent 'Paths_s(x0) models phi-hat' is not well-formed: phi-hat is an LTL formula over abstract states, while Paths_s(x0) is a concrete trajectory or set of trajectories. Please define the induced abstract path via psi and state the implication on that path.","section":"Section 8, Definition 5, Eq. (2)"},{"comment":"The breakpoints B(1) are listed as {0,4,...,40} and B(2) as {0,5,...,50}, but the state space is X=[0,50] x [0,40]; the labels of B(1) and B(2) appear to be swapped.","section":"Section 5, running example"},{"comment":"The text refers to Figure 3 for TPR versus dimension size, but the figure is not included in the manuscript.","section":"Section 9, Figure 3"},{"comment":"There are typos in the surrounding text ('degenrate', 'imrpovement', 'susbtantial', 'mountain care'); please proofread.","section":"Section 9.3, Tables 2 and 3"},{"comment":"The escape probability is denoted q_tau in Eq. (14) and p_tau in the running example; please unify the notation.","section":"Section 7, Eq. (14) and running example"},{"comment":"The 'ground truth' satisfaction set is computed by a dense uniform grid; calling it ground truth overstates its accuracy, since this is itself an abstraction.","section":"Section 9.2, evaluation metrics"}],"recommendation":"major_revision","confidential_remarks":"The self-loop erasure flaw in Section 7 is central and invalidates the experimental claims as presented, but it is correctable by restricting the erasure criterion to one-step escape or by extending the abstraction with time-to-escape information and rerunning the experiments. The sampling-based methods also need to be repositioned as probabilistic rather than conservative-by-construction. I see this as a major revision rather than a reject, provided the authors are willing to make these corrections."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThe paper is a tutorial on the four-step workflow for building conservative discrete abstractions of CPS: grid partition, transition construction (AABB, polytope, sampling with PAC), degenerate-behavior removal, and LTL lifting. The presentation is clear, the three case studies are helpful, and the code is available. It consolidates a lot of known material in one place, and the running unicycle example throughout is a nice pedagogical device.\n\nThe main problem is the self-loop erasure step in Section 7. They certify that every concrete trajectory starting in a cell exits within K steps, and then delete the self-loop. That is only sound if K=1, or if the certificate actually shows no one-step image stays in the cell. For K>1, a trajectory can stay in the cell for the first step and exit later, so deleting the self-loop removes an essential transition and violates condition 3 of Definition 3. The abstraction then under-approximates the concrete dynamics, and the headline claim—conservative-by-construction—no longer holds. This is not a minor technicality: the running example uses K=10, and the erasure is applied in every case study. The fix is straightforward: require one-step escape, or split the cell and erase only the sub-cell that truly exits, or keep the self-loop for states that can remain one step. But as written, the workflow is not sound.\n\nThere is also a bug in Algorithm 2: line 5 uses set intersection instead of union when adding a successor, which would under-approximate transitions even before erasure. That looks like a typo, but it needs fixing.\n\nThe evaluation reports only true positive rate (recall). Given the soundness issue, the absence of false-positive reporting is a real gap—if the abstraction under-approximates, it could verify unsafe states, and they don't measure that.\n\nWhat's genuinely new is modest: the unified four-step presentation and the sampling-based erasure certificate, the latter being a standard binomial PAC bound. The case studies are demonstrations, not new mechanisms. The literature review is decent, and they correctly cite SCOTS, Flow*, and the PAC abstraction work.\n\nWho is this for? Graduate students and practitioners who want a practical walkthrough of abstraction building. They will get value from the structure and the code. But because the central soundness claim is currently broken, I would not trust the workflow as a verification tool until the erasure step is corrected.\n\nRecommendation: send to peer review—a serious referee will catch the flaw and the revision path is clear. But as it stands, I would reject. If the authors fix the erasure criterion and the Algorithm 2 typo, and add false-positive rates, I'd be happy to see it again.\n\nBest,\n[Your name]","headline":"A useful tutorial on building conservative abstractions, but the self-loop erasure step breaks the central soundness guarantee—reject as is, though the fix is clear.","tokens_in":22559,"tokens_out":2761,"would_cite":false,"duration_ms":25230,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"This tutorial establishes a four-step, conservative-by-construction workflow for building finite-state abstractions of cyber-physical systems so that model-checking results transfer back to the original continuous dynamics.","keywords":["conservative abstraction","cyber-physical systems","linear temporal logic","model checking","PAC guarantee","self-loop erasure","CEGAR","state-space quantization"],"falsifier":"Find a cell C and dynamics f such that every trajectory starting in C leaves C within K steps, yet there is some x in C with f(x) also in C. Under the self-loop erasure rule, the transition (C, C) would be deleted even though it represents a genuine one-step behavior, violating Condition 3 of Definition 3. A reader can search for such a cell in a one-dimensional piecewise-linear map, which would refute the erasure rule as stated in Section 7.","tokens_in":21501,"feed_emoji":"⚙️","tokens_out":7087,"duration_ms":64989,"temperature":0.7,"pith_summary":"This tutorial paper establishes a sound-by-construction workflow for turning a continuous cyber-physical system into a finite-state model whose verification results transfer back to the real system. The central promise is that if the finite abstraction satisfies a suitably lifted temporal-logic specification, then the original system satisfies the original specification, making false positives impossible. The workflow is modular, with interchangeable subroutines for partitioning the state space, building transitions via bounding boxes, polytopes, or sampling with a PAC certificate, purging degenerate behaviors, and lifting LTL specifications through may-must semantics. The authors demonstrate the pipeline on three case studies and show that less conservative transition construction yields higher verification accuracy.","feed_headline":"Four-step recipe makes finite models vouch for continuous systems","feed_subtitle":"A conservative-by-construction pipeline transfers model-checking results back to the real dynamics.","key_machinery":"The load-bearing mechanism is the conservative abstraction pair (Definition 3) combined with the may/must homomorphism rho that translates concrete atomic predicates to may-and-must forms over abstract cells. Definition 3 requires that every concrete state and every concrete one-step transition be represented in the finite transition system, and the translation maps each atomic proposition p to a must-predicate on an abstract cell (true only when every concrete state in the cell satisfies p) and each negation not-p to not of a may-predicate, preserving the implication from abstract satisfaction to concrete satisfaction. The missing-mass upper bound supplies the PAC certificate that underpins the sampling-based transition construction.","core_discovery":"The paper's central claim is that its four-step pipeline—state-space quantization, conservative transition construction, degenerate-behavior purging, and may-must LTL lifting—produces a conservative abstraction in the sense of Definition 3, for which Definition 5 holds: if the lifted LTL formula is satisfied by all abstract paths from an abstract initial state, then every concrete trajectory from the corresponding concrete initial set satisfies the original formula. Equivalently, the abstraction cannot verify a property that the concrete system violates. For deterministic transition construction using axis-aligned boxes or polytopes, this is an exact guarantee; for sampling-based construction, it holds with a PAC certificate that bounds the probability mass of unobserved transitions.","pith_inferences":["Beyond the paper, the may-must lifting is not limited to LTL: the same homomorphic translation could lift safety and liveness properties in other branching-time logics by applying may/must at the state-quantifier boundary, though the paper does not develop this.","The K-step exit certificate for self-loop erasure is sufficient but not necessary; a testable extension is a weaker certificate that only requires the measure of states with one-step self-transitions to be negligible, which would allow erasing more self-loops while preserving coverage of one-step behaviors.","The PAC transition certificate could be generalized to non-uniform sampling distributions via importance weighting, letting abstract builders concentrate samples in high-risk regions of the state space.","The pipeline's modularity suggests it can be stress-tested on stochastic cyber-physical systems, where the transition relation would carry probabilistic weights and the lifted specification would need probabilistic semantics."],"forward_implications":["A model checker working on a finite abstraction can be used to certify safety and liveness properties of a continuous closed-loop system, provided the abstraction is built by the four-step construction.","Engineers can choose among bounding-box, polytope, and sampling transition builders as a trade-off between conservatism, runtime, and verification accuracy; the case studies show polytope and sampling methods give higher true-positive rates.","Certified self-loop erasure and counterexample-guided abstraction refinement remove spurious behaviors without sacrificing soundness, which improves verification outcomes for liveness specifications.","The workflow is a teachable template: each step has interchangeable subroutines, so the overall guarantee transfers as long as the chosen subroutine meets its local certificate."],"supporting_citations":[{"why":"Defines the conservative abstract model (Definition 3) and supplies the counterexample-guided abstraction refinement loop for hybrid systems that the paper adapts.","marker":"[13]"},{"why":"Provides the McAllester-Schapire upper bound on missing mass that powers the PAC certificate for sampling-based transition construction.","marker":"[31]"},{"why":"Supplies the growth-bound axis-aligned bounding-box over-approximation method for nonlinear dynamics.","marker":"[32]"},{"why":"Supplies the Taylor-model reachability over-approximation used as an alternative transition-construction technique.","marker":"[11]"},{"why":"Introduces counterexample-guided abstraction refinement, the iterative procedure the paper uses to purge spurious transitions.","marker":"[14]"},{"why":"Establishes the model-checking semantics and exhaustive state-space exploration that the abstraction pipeline relies on.","marker":"[4]"}],"fun_headline_variants":["Four-step recipe for sound finite abstractions in CPS","PAC-certified abstraction pipeline proves CPS properties soundly","Finite-state models that provably capture continuous behavior","Sound abstraction pipeline: finite worlds, real guarantees","Conservative abstraction transfers CPS checks to real dynamics"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The subroutine that erases self-loops assumes that if every concrete trajectory starting in a cell exits that cell within K steps, then deleting the cell's self-loop cannot drop any real one-step behavior; if this certification is only asymptotic or probabilistic, the abstraction may lose conservatism.","fun_headline_variants_meta":{"raw":{"variants":["Four-step recipe for sound finite abstractions in CPS","PAC-certified abstraction pipeline proves CPS properties soundly","Finite-state models that provably capture continuous behavior","Sound abstraction pipeline: finite worlds, real guarantees","Conservative abstraction transfers CPS checks to real dynamics"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001257,"raw_usage":{"total_tokens":5131,"prompt_tokens":909,"completion_tokens":4222,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":525,"completion_tokens_details":{"reasoning_tokens":4149}},"tokens_in":525,"tokens_out":4222,"duration_ms":30377,"temperature":1.0,"reasoning_tokens":4149,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T04:11:35.509192+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find a cell C and dynamics f such that every trajectory starting in C leaves C within K steps, yet there is some x in C with f(x) also in C. Under the self-loop erasure rule, the transition (C, C) would be deleted even though it represents a genuine one-step behavior, violating Condition 3 of Definition 3. A reader can search for such a cell in a one-dimensional piecewise-linear map, which would refute the erasure rule as stated in Section 7.","supporting_citations":[{"cited_title":"In: Goos, G., Hartmanis, J., Van Leeuwen, J., Garavel, H., Hatcliff, J","cited_arxiv_id":null,"evidence_quote":"Defines the conservative abstract model (Definition 3) and supplies the counterexample-guided abstraction refinement loop for hybrid systems that the paper adapts."},{"cited_title":"In: Proceedings of the Thirteenth Annual Conference on Computational Learning Theory","cited_arxiv_id":null,"evidence_quote":"Provides the McAllester-Schapire upper bound on missing mass that powers the PAC certificate for sampling-based transition construction."},{"cited_title":"In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control","cited_arxiv_id":null,"evidence_quote":"Supplies the growth-bound axis-aligned bounding-box over-approximation method for nonlinear dynamics."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the Taylor-model reachability over-approximation used as an alternative transition-construction technique."},{"cited_title":"In: Emerson, E.A., Sistla, A.P","cited_arxiv_id":null,"evidence_quote":"Introduces counterexample-guided abstraction refinement, the iterative procedure the paper uses to purge spurious transitions."},{"cited_title":"MIT Press, Cambridge, MA, USA (Apr 2008)","cited_arxiv_id":null,"evidence_quote":"Establishes the model-checking semantics and exhaustive state-space exploration that the abstraction pipeline relies on."}],"review_version":1}