{"id":"dfbb306e-15d4-4a6d-9c7f-8589618f507d","arxiv_id":"2508.03627","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"LEAP is a state-merging algorithm that passively learns event-recording automata from positive and negative symbolic timed words, with an NP-completeness result for the merge check and a completeness proof via characteristic samples.","lead":"Researchers built LEAP, an algorithm that learns a timed system model from examples the user marks as good or bad, given as symbolic time-stamped scenarios. It is the first passive learner for event-recording automata and proves that every model in this class can be recovered from a characteristic set of examples.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Completeness rests on an unproved import, [13, Lemma 19], which is fragile under this paper's empty-word convention; a small DERA shows the same-state/tail property is not automatic, so Theorem 13 is only as secure as that citation.","rationale":"The reader's weakest assumption is exactly the unproved transfer of [13, Lemma 19], and my reading of Section 5 confirms that Lemma 16, Corollary 19, and Theorem 13 all rest on it. The example above shows the property is not a formal consequence of plain DERA determinism together with the paper's empty-word convention, so it cannot be left as an implicit folklore fact; the paper should either prove the adapted lemma or add an explicit hypothesis. This does not overturn the algorithmic construction or the SMT implementation, which are independently sensible, but it raises the correctness risk of the completeness half of the central claim, matching the CONDITIONAL verdict. I also noticed a separate, real correctness issue: the abstract states that determining whether two states can be merged while preserving sample consistency is NP-complete, whereas the proved result is NP-completeness of the intersection-non-emptiness problem; the merge-permissibility decision is the complementary universal question and appears to be coNP-complete. That is a distinct concern and does not change the verdict.","tokens_in":29044,"tokens_out":31519,"duration_ms":398350,"concrete_test":"Obtain [13, Lemma 19], restate it in this paper's K-constraint notation, and check the small DERA above against [13]'s formal definition of simple DERA. Independently, run a bounded exhaustive search over DERAs with at most 5 states, alphabet {a,b}, K≤2, filtering those satisfying [13]'s simple-DERA conditions, and test every pair of region words reaching the same state against every region suffix w for the condition Ju.wK≠∅ ⇔ Jv.wK≠∅. A single admitted counterexample refutes Lemma 16; if the enumeration is exhaustive and finds none, the cited property is credible for the ERA class as defined here.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Lemma 16, the step that makes the characteristic-set construction finite, is proved by importing [13, Lemma 19]: every ERA language has a simple DERA in which any two region words reaching the same state have identical non-emptiness tails, i.e. for every suffix w, Ju.wK is non-empty iff Jv.wK is non-empty. The paper neither states nor proves this lemma, and the property is subtle under its definitions. On page 17 the paper declares that every empty region word, one with JwK=∅, belongs to every timed language. Under that convention, two prefixes can reach the same control state with different current clock regions and still have different tails even though the state's future timed language is the same. Concretely, for K=2, a DERA with q0 --a,(xa=0∧xb=0)--> q1; q1 --a,(xa∈(0,1)∧xb∈(0,1))--> q2 and q1 --a,(xa>2∧xb>2)--> q2; q2 --b,(xa=0∧xb∈(0,1))--> q_rej and q2 --b,(xa=0∧xb>2)--> q_acc has u=(a,xa=0∧xb=0)(a,xa∈(0,1)∧xb∈(0,1)) and v=(a,xa=0∧xb=0)(a,xa>2∧xb>2) both reaching q2, while for w=(b,xa=0∧xb∈(0,1)), u.w is non-empty and rejected but v.w is empty and hence in L. Thus TL(u)≠TL(v) despite the common state. Whether [13]'s definition of simple DERA, for instance its global path-satisfiability condition, excludes this automaton is exactly the missing argument; if it does not, Lemma 16 and with it Theorem 13 collapse.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces LEAP, a state-merging algorithm for passively learning event-recording automata (ERA) from positive and negative symbolic timed words. LEAP builds a prefix tree from the positive sample, then repeatedly attempts to merge frontier states with red states, allowing the merge only if the resulting automaton remains consistent with the negative sample; the consistency check is reduced to an SMT problem. The paper proves that the underlying intersection non-emptiness problem for an ERA and a symbolic word is NP-complete even for deterministic ERA, gives a polynomial case for region words, and proves a completeness result: for every ERA-recognizable language there exists a finite characteristic sample set of region words on which LEAP returns a DERA for exactly that language. An implementation is evaluated against active learning tools on several benchmarks, and an artifact is provided.","tokens_in":29469,"tokens_out":23763,"duration_ms":295855,"significance":"If the completeness proof is made fully rigorous, this is a solid contribution to timed automata learning. The paper provides the first passive learner for ERA from symbolic timed words, with an identification-in-the-limit guarantee for the whole ERA class, together with a clean NP-completeness result that justifies the SMT-based merge check. The authors explicitly exploit nondeterminism and symbolic (zone-like) words to obtain compact automata, and they provide an open-source implementation and an artifact. The experiments give useful evidence that handling symbolic words directly can outperform region-based splitting on practical benchmarks. The main novelty — a language-theoretic characteristic-set construction for a class without unique minimal automata — is interesting and potentially extendable.","major_comments":[{"comment":"Theorem 4 states the wrong side of the consistency condition for negative samples: it claims that for every w∈S−, JwK∩L(A)≠∅, whereas consistency with a negative sample requires JwK∩L(A)=∅. The proof sketch and the merge-check description on page 8 use the correct (empty) direction, so this is likely a typo, but it appears in a central statement and must be corrected.","section":"Section 3.2, Theorem 4"},{"comment":"Lemma 16 is load-bearing for the completeness theorem: it is used to infer that the set of tails {TL(u) | u∈RW(Σ,K)} is finite, which is what makes the characteristic sets of Corollary 19 and Theorem 13 finite. The proof is not self-contained: it invokes 'Lemma 19 of [13]' without stating that lemma or proving that it applies to the definitions used here. In particular, the paper's convention that empty region words belong to every language interacts with the tail definition, and the claimed property that two region words reaching the same state have identical non-emptiness tails for all suffixes is not a formal consequence of the definitions given in the paper. A concrete DERA with K=2 illustrates the risk: let q0 go to q1 on (a, xa=0∧xb=0), let q1 go to q2 on (a, xa∈(0,1)∧xb∈(0,1)) and also on (a, xa>2∧xb>2), and let q2 go to a rejecting state on (b, xa=0∧xb∈(0,1)) and to an accepting state on (b, xa=0∧xb>2). The region words u=(a,xa=0∧xb=0)(a,xa∈(0,1)∧xb∈(0,1)) and v=(a,xa=0∧xb=0)(a,xa>2∧xb>2) both reach q2, yet for w=(b,xa=0∧xb∈(0,1)) the word u.w is non-empty and rejected while v.w is empty and hence, by the paper's convention, in L. Thus TL(u)≠TL(v) even though the two prefixes reach the same state. The authors must either state and prove the imported property for their exact SDERA notion, or give a direct proof of Lemma 16; without this, Theorem 13 is not established.","section":"Section 5, Lemma 16"},{"comment":"In the final paragraph of the proof of Theorem 13, the reverse inclusion L⊆L(A_n) uses the sentence 'from Lemma 26(5) we know that δn(qin,w′)=δn(qin,t′)' to conclude that two tails-equal prefixes reach the same state. Lemma 26(5), however, is stated for a pair consisting of one red and one non-red state in an intermediate automaton A_i. In the final automaton A_n all states are red, so the lemma does not apply. The needed statement is the converse direction — equal tails imply the same state for red states — which the paper neither states nor proves. Since this step is essential for the contradiction that shows w∈L(A_n), the proof of Theorem 13 is incomplete as written.","section":"Section 5, proof of Theorem 13"}],"minor_comments":[{"comment":"The paper asserts that the proof of [28] for DTA 'also holds for the class of ERA, by relabeling' but gives no relabeling argument, and the step from non-polynomial learnability to the nonexistence of polynomial-size characteristic sets for LEAP is asserted without proof. This is a secondary claim, but it should be substantiated or softened.","section":"Section 5, Lemma 11 and Corollary 12"},{"comment":"The convention that every empty region word belongs to every timed language is unusual and is central to the tail argument; it should be introduced as a formal definition, and its effect on tail languages and on the consistency of samples should be discussed explicitly.","section":"Section 5, Definition 15 and Remark 22"},{"comment":"The proof says that checking JwK≠∅ suffices; this is correct only because the word is a region word and the automaton is complete over regions, so the path is syntactically determined. This assumption should be stated explicitly in the proof.","section":"Section 4, Lemma 9"},{"comment":"The table compares the number of samples for passive LEAP with the number of queries for active learners. The text acknowledges the different settings, but the table would benefit from a note making explicit that the columns are not directly comparable measures of data efficiency.","section":"Section 6, Table 1"}],"recommendation":"major_revision","confidential_remarks":"The central idea is promising and the NP-completeness part appears solid, but the completeness proof currently depends on an unstated external lemma and contains a final-step gap in the proof of Theorem 13. I recommend requesting a fully self-contained proof of Lemma 16 and a clarification of the reverse-inclusion argument before reconsidering the paper."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This is a serious paper. The state-merging algorithm LEAP is genuinely new, the NP-completeness of intersection non-emptiness for DERA/ERA is a real contribution, and the authors back it with an SMT-based implementation and a completeness argument via characteristic sets. They also ship code and an artifact, which is more than many theory papers do. The L_n example showing succinct nondeterministic ERA over determinized versions is a nice empirical touch. If I worked on timed automata learning, I would want to know about this work.\n\nThe soft spots are real but not fatal, except one. First, Theorem 4 states the wrong direction for negative samples: it says L(A) ∩ JwK ≠ ∅ for all w ∈ S−, but the surrounding text and the merge check clearly intend empty intersection. That is an obvious typo, but it is in a theorem statement and should be fixed before publication. Second, the empirical section compares only against active learners; there is no passive baseline, and the query-count comparison is not apples-to-apples. That is defensible given that no other passive symbolic-word ERA learner exists, but the authors should acknowledge the mismatch more explicitly.\n\nThe load-bearing concern is the completeness proof. Lemma 16, which makes the characteristic-set construction finite, is proved entirely by importing Lemma 19 of [13] to assert the existence of a simple DERA where same-state regions have identical non-emptiness tails. The paper neither states nor proves that lemma, and it is fragile under the paper's convention that every empty region word (JwK = ∅) belongs to every timed language. Under that convention, two prefixes can reach the same control state with different current clock regions, yet have different tails simply because one continuation is empty (hence in the language) and the other is non-empty and rejected. I checked the concrete DERA from the stress-test note: it is small, has satisfiable accepting paths, and does exactly this. If the cited property from [13] does not hold for the ERA class as defined here, then Lemma 16, Corollary 19, and Theorem 13 all collapse. At minimum, the authors need to state and prove the imported lemma in their own setting, or modify the empty-word convention so the same-state/tail property is not vacuous.\n\nThe reduction for NP-hardness looks plausible, and the SMT encoding is standard. The citation pattern is clean: self-citations are only baselines, and the main results are not derived from the authors' own prior work.\n\nThis paper deserves a serious referee. The central algorithm and complexity result stand on their own, and the completeness proof is a genuine attempt that might be repairable. I would send it to peer review, but the reviewer report must push hard on Lemma 16 and the empty-word convention.","headline":"A genuinely new passive learner for ERA from symbolic timed words, with a plausible NP-completeness result, but the completeness theorem leans on an unproved imported lemma that may not survive the paper's own empty-word convention.","tokens_in":29953,"tokens_out":2458,"would_cite":true,"duration_ms":33669,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q45","68Q32","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that a state-merging algorithm, LEAP, can passively learn every ERA-definable timed language from positive and negative symbolic timed words, checking each merge by SMT despite the NP-complete consistency problem.","keywords":["event-recording automata","passive learning","state-merging","symbolic timed words","timed languages","characteristic sets","NP-completeness","SMT solving"],"falsifier":"Exhibit a K-ERA-recognizable language and two region words u and v that lead to the same state of its minimal simple DERA, together with a suffix w such that exactly one of Ju.wK and Jv.wK is empty; this directly contradicts the property from [13] on which Lemma 16 and Theorem 13 depend, and a small search over ERA benchmarks could look for it.","tokens_in":28857,"feed_emoji":"⏱️","tokens_out":7950,"duration_ms":83226,"temperature":0.7,"pith_summary":"This paper establishes that a useful class of timed languages, those definable by Event-Recording Automata (ERA), can be learned passively from examples. LEAP, the proposed algorithm, takes positive and negative symbolic timed words—event sequences whose positions carry timing constraints—and returns an ERA that is consistent with the sample. The main theoretical claim is completeness: for every ERA-recognizable language there exist finite characteristic sample sets for which LEAP returns an ERA accepting exactly that language. Because ERA are determinizable and complementable, this opens a route to deriving timed requirement specifications from high-level scenarios rather than from raw timed execution logs.","feed_headline":"Passive algorithm learns event-recording automata from timed examples","feed_subtitle":"It merges states from symbolic timed examples and provably recovers every ERA-definable language.","key_machinery":"The load-bearing machinery is the state-merging loop of LEAP, adapting RPNI to the timed setting: a prefix tree over symbolic timed words, a total order that fixes which frontier node is processed next, and a fold operation that recursively merges successors after a successful merge. Each candidate merge is filtered through an SMT encoding of the intersection non-emptiness problem for an ERA and a symbolic word. For completeness, the key objects are tail languages TL(u), the set of region-word suffixes w such that u.w lies in the target language, together with a structural property of simple deterministic ERA taken from the literature: region words reaching the same state must agree, for every suffix, on whether the concatenation is satisfiable. Lemma 16 uses that property to show the set of distinct tails is finite, and the characteristic-set construction uses shortest prefixes and a kernel of one-step extensions to force LEAP to reproduce the target tails.","core_discovery":"On the paper's own terms, the central discovery is that passive identification from symbolic timed words is complete for the class of ERA languages. LEAP starts from a prefix tree of the positive samples, then repeatedly merges a blue frontier node into a red state whenever the resulting ERA still rejects all negative words; because symbolic guards can overlap, deciding whether a merge is safe is NP-complete, and the paper encodes that decision as an SMT instance. Theorem 4 guarantees that LEAP terminates and returns an ERA consistent with the sample, while Theorem 13 guarantees that for every K-ERA-recognizable language L there is a characteristic sample set S of region words such that LEAP outputs a deterministic ERA with L(A)=L. The proof is language-theoretic: tails TL(u) of region words are shown to be finite and to determine when state merging is safe, which lets the characteristic set enforce that every merge in LEAP preserves the target language.","pith_inferences":["The tail-based completeness argument does not rely on a unique minimal automaton, so a natural extension is to adapt it to other timed model classes with a region-like canonical form, such as deterministic timed automata with resets.","A concrete test of the paper's load-bearing premise is to search ERA benchmarks for a language whose minimal simple DERA violates the same-state/same-satisfiability-tail property; if one exists, the completeness theorem fails even though the algorithm's consistency guarantee survives.","The paper's interactive use case suggests a practical measure: how few natural-language scenarios, possibly generated by a language model and vetted by an engineer, are enough for LEAP to converge to the intended ERA compared with active-learning query counts.","Scaling LEAP to large samples will hinge on the SMT encoding of merge checks; a specialised difference-constraints solver for the region-word case could avoid the exponential blowup observed when zone words are split into region words."],"forward_implications":["For every ERA-definable language, some finite sample of positive and negative region words makes LEAP return a deterministic ERA for exactly that language, so passive learning of ERA is complete in the limit from symbolic data.","Because LEAP may keep nondeterminism, it can represent some languages with exponentially fewer states than any deterministic learner; the paper demonstrates this with the L_n family, where n+2 states suffice.","The merge-consistency test is NP-complete for general symbolic words but polynomial when the samples are region words and the current automaton is deterministic, so the computational cost of LEAP depends sharply on the input representation.","No polynomial-size characteristic set built from region words can exist for all ERA languages, since the class is not polynomially learnable; the guaranteed sample sets may need to be exponential.","Working directly with symbolic zone words keeps the sample size small and insensitive to the maximal constant K, which the experiments show lets LEAP scale to benchmarks where the region-word version times out."],"supporting_citations":[{"why":"supplies the RPNI state-merging scheme that LEAP adapts to timed languages.","marker":"[20]"},{"why":"provides the simple-DERA construction and the property that region words reaching the same state have identical satisfiability behaviour for all suffixes, on which the completeness proof rests.","marker":"[13]"},{"why":"defines event-recording automata and their determinizability and complementability properties.","marker":"[4]"},{"why":"supplies the timed-automata semantics and the region/clocked-word background used throughout.","marker":"[2]"},{"why":"formulates identification in the limit and motivates the characteristic-set completeness criterion.","marker":"[12]"},{"why":"shows ERA are not polynomially learnable, which forces the characteristic sets in Corollary 12 to be exponential in the worst case.","marker":"[28]"},{"why":"gives the 3-SAT problem used as the source for the NP-hardness reduction of the intersection non-emptiness problem.","marker":"[8]"},{"why":"is the active-learning ERA tool used as an empirical baseline in the evaluation.","marker":"[19]"}],"fun_headline_variants":["Passive algorithm learns event-recording automata from timed samples","LEAP merges states to infer event-recording automata from words","NP-complete merge check tamed by SMT in passive ERA learning","Complete passive inference for event-recording automata from samples","From timed examples to event-recording automata by state merges"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The completeness proof depends on a cited structural property of event-recording automata: any two region words that lead to the same state must agree, for every possible continuation, on whether the continuation can be realised by an actual timed word; if that property fails for some ERA language, the finiteness of tails and the whole characteristic-set construction collapse.","fun_headline_variants_meta":{"raw":{"variants":["Passive algorithm learns event-recording automata from timed samples","LEAP merges states to infer event-recording automata from words","NP-complete merge check tamed by SMT in passive ERA learning","Complete passive inference for event-recording automata from samples","From timed examples to event-recording automata by state merges"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000331,"raw_usage":{"total_tokens":1786,"prompt_tokens":828,"completion_tokens":958,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":444,"completion_tokens_details":{"reasoning_tokens":868}},"tokens_in":444,"tokens_out":958,"duration_ms":10102,"temperature":1.0,"reasoning_tokens":868,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T04:19:09.208331+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a K-ERA-recognizable language and two region words u and v that lead to the same state of its minimal simple DERA, together with a suffix w such that exactly one of Ju.wK and Jv.wK is empty; this directly contradicts the property from [13] on which Lemma 16 and Theorem 13 depend, and a small search over ERA benchmarks could look for it.","supporting_citations":[{"cited_title":"Learning of event-recording automata","cited_arxiv_id":null,"evidence_quote":"provides the simple-DERA construction and the property that region words reaching the same state have identical satisfiability behaviour for all suffixes, on which the completeness proof rests."},{"cited_title":"Henzinger","cited_arxiv_id":null,"evidence_quote":"defines event-recording automata and their determinizability and complementability properties."},{"cited_title":"Mark Gold","cited_arxiv_id":null,"evidence_quote":"formulates identification in the limit and motivates the characteristic-set completeness criterion."},{"cited_title":"Polynomial distinguishability of timed automata","cited_arxiv_id":null,"evidence_quote":"shows ERA are not polynomially learnable, which forces the characteristic sets in Corollary 12 to be exponential in the worst case."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"gives the 3-SAT problem used as the source for the NP-hardness reduction of the intersection non-emptiness problem."},{"cited_title":"Greybox learning of languages recognizable by event-recording automata","cited_arxiv_id":null,"evidence_quote":"is the active-learning ERA tool used as an empirical baseline in the evaluation."}],"review_version":1}