{"id":"2484703e-3253-4192-a968-6cd555f00b33","arxiv_id":"2501.16274","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":2.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"This is a structured survey and qualitative comparison of recent algorithms for learning LTL specifications from positive and negative behavioral examples.","lead":"This paper surveys computer programs that automatically learn LTL specifications, the formal rules used in verification, from examples of good and bad system behavior. It groups these programs into three families and compares what each one guarantees, so engineers can choose a method.","discovery_kind":"review","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Table 1 compares 'sound, complete, minimal' claims without fixing trace semantics; until each row is classified as finite- or infinite-trace LTL, the central comparative claim is under-specified.","rationale":"I read the survey as a scoping comparison rather than a proof-bearing research paper. The reader's weakest assumption—selection without a protocol—is real, but I found a more specific, internal flaw in the comparison itself. Section 2.2 defines two different satisfaction relations (infinite words and finite words), and Definition 1 does not choose one; Table 1's rows are then compared along guarantee dimensions that are semantics-dependent. This is load-bearing because the abstract's claim that the survey lets practitioners compare state-of-the-art techniques is only true if the rows solve the same problem. The finite/infinite distinction is not cosmetic: LTL over finite traces has different expressive and canonical properties, and minimality can differ. The paper's own text shows the ambiguity: it motivates LTL for reactive systems (infinite behavior) yet describes encodings and examples that are naturally finite. Since the survey performs no implementation, the only evidence for cross-row comparability is the original papers' self-descriptions, and the survey does not reconcile those descriptions with a single semantics. If my proposed check shows every row uses finite traces, the taxonomy remains useful and the paper can be accepted as an LTLf-focused scoping review; if rows mix semantics, the comparison needs revision. I agree with the reader that a conditional verdict is appropriate; my concern does not move the verdict, but it points to a different repair than the reader's suggested selection methodology.","tokens_in":15443,"tokens_out":5998,"duration_ms":63605,"concrete_test":"For each work in Table 1, read the original paper's definitions and record: (i) word domain, i.e. finite traces, infinite words, or both; (ii) whether positive and negative examples are finite sets of finite words or infinite-word acceptance conditions; and (iii) the exact size measure used for 'minimal'. Then rebuild Table 1 with a 'Trace semantics' column. If any row's guarantee changes when the semantics is fixed—for example, completeness holds only for finite traces, or 'full LTL' is actually 'LTLf'—the comparative conclusions in Sections 4–6 must be rephrased to avoid cross-semantics comparisons. A minimal check: for the rows claiming 'complete, minimal', re-derive the completeness theorem under both finite and infinite semantics; if completeness holds only for finite traces, Table 1's 'full LTL' cell is misleading.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The survey's central claim is that the field can be usefully organized into constraint-, enumeration-, and neural-network-based approaches with the guarantees and input settings summarized in Table 1. That claim depends on Table 1's rows being comparable instances of one learning problem. The paper never establishes this. Section 2.2 defines semantics both for infinite words over Σ^ω and for finite words over Σ^*, and Definition 1 leaves the word domain implicit; Table 1 then reports 'full LTL', 'sound, complete, minimal', etc., without recording which semantics each method targets. Minimality is semantics-relative: a formula that is minimal for LTLf over finite traces need not be minimal for LTL over infinite words, and consistency on finite samples does not constrain behavior on infinite suffixes. The surrounding text reinforces the ambiguity: Section 4 discusses bounded model checking encodings and finite-trace examples, while the abstract motivates LTL for reactive systems, whose executions are infinite. If some rows are LTLf and others are full LTL, the comparison mixes different problems and the guarantee column cannot be read as a single ranking. The paper also relies on each cited paper's self-reported guarantees without reimplementation, so an unstated semantic mismatch would propagate into Table 1. The 'survey is correct' conditional in the abstract therefore fails at the point where the comparison is defined.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper is a survey of passive learning of Linear Temporal Logic specifications from examples of system behavior. It organizes recent work into three families — constraint-based (SAT/SMT/MaxSAT/ASP), enumeration-based, and neural-network-based — and compares eleven selected works in Table 1 on the dimensions of technique, LTL fragment, input data (positive/negative, perfect/noisy), and theoretical guarantees (soundness, completeness, minimality). The paper also covers extensions: learning from noisy data, positive-only data, template-based mining, translation from natural language, and other temporal logics (STL, CTL, MTL, PSL). The intended contribution is an accessible map of the area for formal methods practitioners.","tokens_in":15661,"tokens_out":8083,"duration_ms":71296,"significance":"The survey fills a useful gap: the LTL specification mining literature is growing quickly and lacks a single entry point. The three-way taxonomy is sensible, and the background in Section 2 is standard. The paper is particularly helpful in explaining the syntax-DAG representation and the folk theorem that minimality is what makes the learning problem non-trivial. The table and accompanying narrative, once corrected for trace semantics, would let practitioners identify which tool families fit their input format and guarantee needs. Since this is a survey, there are no machine-checked proofs or benchmarks to credit, but the presentation is generally clear and the referencing is broad. The main value is organizational, and that value depends on the comparability of Table 1's rows.","major_comments":[{"comment":"The paper never fixes the trace semantics for the learning problem. Definition 1 leaves the word domain implicit, and Section 2.2 presents both infinite-word and finite-word semantics without saying which one applies to the rest of the paper. This matters because the guarantees listed in Table 1 — soundness, completeness, minimality — are semantics-relative: a formula that is minimal for LTLf over finite traces need not be minimal for full LTL over infinite words, and consistency on finite examples does not constrain behavior on infinite suffixes. The problem is visible in Table 1 itself: Luo et al. [56] and Wan et al. [81] are listed under \"full LTL\", but the titles of the cited papers state they learn LTLf formulas (LTL over finite traces). The authors should add a semantics dimension (e.g., LTL over infinite words vs. LTLf) to Table 1, correct the fragment labels, and explain how \"minimal\" is defined for each row.","section":"§2.2 / Definition 1 / Table 1"},{"comment":"The survey claims in the abstract and conclusion to \"list and compare recent advances\" and to provide a \"comprehensive overview\", but it gives no search protocol, inclusion/exclusion criteria, or time window for selecting the eleven works in Table 1. Without such criteria the reader cannot determine whether the three-way taxonomy and the qualitative conclusions are representative of the field or merely reflect a convenience sample. At a minimum, the paper should state its selection criteria and scope; alternatively, it should soften the comprehensiveness claim to one about a representative subset.","section":"§3, §8, Table 1"}],"minor_comments":[{"comment":"The sentence \"it suffers from the limitation that the extracted LTL formula might accurately capture the behavior of the trained GNN\" should read \"might not accurately capture\"; as written it asserts a non-limitation.","section":"§6"},{"comment":"In the definition of w[i:], \"the suffix starting from the starting from position i\" contains a duplicated phrase.","section":"§2.1"},{"comment":"The phrase \"the authors solve formulate a learning task\" contains a typo; it should be \"the authors formulate a learning task\".","section":"§4.2"},{"comment":"The word \"potenitally\" is misspelled in the last sentence of Section 4.1.","section":"§4.1"},{"comment":"Z3 is an SMT solver, not specifically a SAT solver; the text should say \"SAT/SMT solver\" or \"SMT solver\" when referring to it.","section":"§4"},{"comment":"The finite-word Until clause is typeset as \"i≤ j≤| w− 1|\"; the bars around w are misplaced and should read \"i ≤ j ≤ |w| − 1\".","section":"§2.2"},{"comment":"References [13] and [14] are the same paper (Bombara et al., HSCC 2016) and appear twice with identical bibliographic data; one duplicate should be removed.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The manuscript fits the scope of a formal methods venue. One editorial concern: a substantial share of the table entries and described approaches come from the authors' own groups (e.g., [60], [69], [32], [75], and related works [70], [57], [71]). This is not improper in a survey, but the authors should be encouraged to state their selection criteria explicitly and to apply the same critical scrutiny to their own entries as to others; the current text is noticeably more detailed and less critical for those entries."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First thing to know: this is a solid survey, not a research contribution. It doesn't introduce new algorithms or data, but it gives the FM community a compact map of passive LTL mining, and the three-way split into constraint-based, enumeration-based, and neural-network methods is a sensible organizing principle. The descriptions of the archetypal SAT encoding (Neider-Gavran, Riener) and the enumeration approach (Raha et al.) are accurate and helpful.\n\nWhere it earns its keep: the discussion of the common structure across constraint-based methods (syntax DAG encoding plus BMC-style consistency constraints) is well done, and the coverage of noisy data, positive-only examples, templates, natural language, and neighboring logics gives a good sense of the landscape. The LTL preliminaries are standard but correct.\n\nThe soft spots are real but mostly fixable. The biggest one is Table 1: it lists 'full LTL' and 'sound, complete, minimal' without fixing whether each method targets finite traces (LTLf) or infinite traces (LTL). Minimality is semantics-relative—a minimal formula for LTLf need not be minimal for LTL—and consistency on finite samples doesn't constrain behavior on infinite suffixes. The survey defines both semantics in Section 2.2 but never connects those definitions to the rows of Table 1, so the guarantee column can't be read as a single ranking. The stress-test note is right about this; it's not a manufactured flaw. I'd call it a presentation/comparability gap rather than a load-bearing one, but it matters for anyone trying to pick a tool.\n\nSecond, the selection of the eleven works is informal—no search protocol, no exclusion criteria—and it leans on the authors' own work. That's not misconduct, but it undercuts the word 'comprehensive' in the title and the reader's ability to trust the coverage. Third, all guarantees are taken from the cited papers with no independent check, so Table 1 is a map of self-reported properties. That's normal for a survey, but worth stating.\n\nOne more thing: the paper is a published book chapter (ref [61] is the same text), so as a fresh submission it would have a duplication problem. For an arXiv reader, that's fine; for a venue expecting new content, it isn't.\n\nBottom line: a useful orientation for newcomers and practitioners, with some honest caveats. With a fixed Table 1 (label LTL vs LTLf per row) and a transparent selection methodology, it would be a legitimate peer-reviewed survey. As is, I'd still send it to review if the venue does surveys, but I'd tell the authors to address the semantics issue before acceptance.","headline":"Useful, readable survey of LTL specification mining, but the comparative table under-specifies trace semantics and the work is already a published book chapter.","tokens_in":16219,"tokens_out":3381,"would_cite":true,"duration_ms":32578,"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 survey organizes recent algorithms for mining Linear Temporal Logic specifications from example behaviors into three families — constraint-based, enumeration-based, and neural-network-based — and compares the guarantees each family…","keywords":["linear temporal logic","specification mining","passive learning","formal verification","constraint-based search","enumeration-based search","graph neural networks","survey"],"falsifier":"Run the surveyed tools on a shared benchmark of labeled traces and compare each result with its Table 1 guarantee; a single counterexample sample on which a sound-and-complete tool returns a non-minimal or inconsistent formula would falsify the comparison, and a published LTL-mining approach that fits none of the three search families would falsify the taxonomy's completeness.","tokens_in":15196,"feed_emoji":"🧭","tokens_out":12650,"duration_ms":105755,"temperature":0.7,"pith_summary":"Formal verification depends on formal specifications, but writing them by hand is widely seen as a bottleneck. This survey examines recent work that instead learns specifications automatically, expressed in Linear Temporal Logic (LTL), from examples of desired and undesired system behavior. It tries to establish that these efforts are usefully organized by their search strategy: constraint-based methods that encode the learning problem for off-the-shelf solvers, enumeration-based methods that search the space of formulas directly, and neural-network-based methods that trade formal guarantees for scalability. For a practitioner, the survey's value is a comparison of what each approach can promise — soundness, completeness, minimality, and tolerance for noisy or positive-only data — so the choice of method can be matched to the available examples and required assurance.","feed_headline":"Survey sorts temporal-logic spec mining into three algorithm families","feed_subtitle":"Constraint-based miners keep formal guarantees; enumeration and neural methods trade them for scale.","key_machinery":"The load-bearing object is the syntax directed acyclic graph (syntax DAG) of an LTL formula, which represents shared subformulas so that formula size equals node count. Constraint-based methods use the DAG as the template for SAT/MaxSAT/MILP encodings; enumeration-based methods use partial DAGs and rewrite rules to prune equivalent formulas; neural methods encode words as linear graphs over which graph neural networks propagate satisfaction information of candidate subformulas. The passive-learning definition, with its minimality requirement, is the common yardstick that makes the three families comparable.","core_discovery":"On the survey's own terms, the central discovery is that the passive learning problem — given a sample $S=(P,N)$ of positive and negative words, compute a minimal LTL formula consistent with $S$ — admits three methodological families with distinct trade-offs. Constraint-based approaches encode the syntax of candidate formulas as a syntax DAG and their semantics as bounded-model-checking-style constraints, then call SAT, MaxSAT, MILP, or ASP solvers; under perfect positive/negative data, several of them return sound, complete, and minimal formulas. Enumeration-based approaches search the formula space directly, using dynamic programming, rewrite-rule pruning, or GPU acceleration; individual tools range from sound-only anytime algorithms to a sound, complete, and minimal enumerator, and the family overall trades worst-case minimality for scalability. Neural-network approaches, built on the insight that a word can be viewed as a linear graph, learn via graph neural networks and offer no formal consistency guarantees but are aimed at large noisy datasets. The comparison table condenses the surveyed works into columns for LTL fragment, classification of positive and negative examples, input data, and guarantees, grounding the survey's three-way categorization.","pith_inferences":["A natural next step the survey leaves implicit is to combine the families, for instance using a neural network to propose candidate formulas that a constraint-based verifier then checks or minimizes, since one family's weakness is another's strength.","The positive-only line of work suggests a testable extension: if 'strongness' is formalized as the right optimization criterion, one-class specification miners could be applied to reward-function learning in reinforcement learning, where negative demonstrations are often unavailable.","Because the survey does not propose a common benchmark, an immediate consequence a reader might draw is that the field's next bottleneck is empirical: a shared corpus of labeled traces would let the guarantee claims in Table 1 be tested head-to-head."],"forward_implications":["A practitioner can use Table 1 to match a miner to the data: perfect labeled data admits several sound, complete, and minimal methods, while noisy or positive-only data forces a choice among relaxed, enumerative, or neural approaches with weaker guarantees.","For noisy data, the survey indicates the practical options are MaxSAT-style relaxation in the constraint-based family, enumeration heuristics, or neural networks, with formal guarantees weakening or disappearing in that order.","Enumeration-based and GPU-accelerated approaches are presented as the scalable end of the spectrum, positioning them as the practical choice when formula minimality matters less than throughput.","Neural-network approaches currently provide no consistency guarantees, but the survey suggests that faithful encodings of LTL semantics into the network architecture can at least guarantee that a formula can be extracted from the trained model.","Template-based mining, natural-language-to-LTL translation, and learning in logics beyond LTL (STL, CTL, ATL, MTL, PSL) are adjacent settings that the passive-learning taxonomy does not directly cover but that share the specification bottleneck."],"supporting_citations":[{"why":"Introduces the SAT-based encoding of syntax DAGs and sample consistency that anchors the constraint-based family and the minimality discussion.","marker":"[60]"},{"why":"Provides an alternating-finite-automaton SAT encoding shown to be essentially equivalent to the LTL encoding, corroborating the constraint-based grouping.","marker":"[19]"},{"why":"The Scarlet enumeration tool with dynamic programming and Boolean subset cover is the main representative of the enumeration-based family.","marker":"[69]"},{"why":"Extends the SAT encoding to MaxSAT with hard and soft constraints, grounding the survey's noisy-data comparison.","marker":"[32]"},{"why":"Uses MILP and counterexample guidance to learn from positive examples only, grounding the positive-only setting.","marker":"[22]"},{"why":"Adds strongness as an optimization criterion and uses counterexample-guided SAT search, completing the positive-only comparison.","marker":"[75]"},{"why":"GPU-accelerated enumeration with relaxed unique checks and divide-and-conquer supports the scalability claims for enumeration-based methods.","marker":"[78]"},{"why":"A graph-neural-network approach to LTL formula learning that grounds the neural-network category.","marker":"[56]"},{"why":"A graph-neural-network approach with a faithful LTL encoding, showing reliable formula extraction from trained networks.","marker":"[81]"},{"why":"Syntax-guided synthesis encoding of past-time LTL, illustrating the extension of constraint-based methods to richer fragments and solver frameworks.","marker":"[3]"}],"fun_headline_variants":["Survey sorts LTL spec mining into three algorithm families","LTL spec mining survey: constraint, enumeration, neural trade-offs","Spec mining survey weighs formal guarantees vs scalability","Three LTL spec mining families: which one keeps guarantees?"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The survey's conclusions rest on the works in Table 1 being a representative selection of the field and on those works' self-reported guarantees being accurate, since the paper neither explains a systematic search process nor re-runs the tools.","fun_headline_variants_meta":{"raw":{"variants":["Survey sorts LTL spec mining into three algorithm families","LTL spec mining survey: constraint, enumeration, neural trade-offs","Spec mining survey weighs formal guarantees vs scalability","Three LTL spec mining families: which one keeps guarantees?"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000658,"raw_usage":{"total_tokens":2998,"prompt_tokens":919,"completion_tokens":2079,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":535,"completion_tokens_details":{"reasoning_tokens":2014}},"tokens_in":535,"tokens_out":2079,"duration_ms":14560,"temperature":1.0,"reasoning_tokens":2014,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T13:34:05.760123+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the surveyed tools on a shared benchmark of labeled traces and compare each result with its Table 1 guarantee; a single counterexample sample on which a sound-and-complete tool returns a non-minimal or inconsistent formula would falsify the comparison, and a published LTL-mining approach that fits none of the three search families would falsify the taxonomy's completeness.","supporting_citations":[{"cited_title":"Ltlmop: Experimenting with language, temporal logic and robot control","cited_arxiv_id":null,"evidence_quote":"Extends the SAT encoding to MaxSAT with hard and soft constraints, grounding the survey's noisy-data comparison."},{"cited_title":"Temporal-logic queries","cited_arxiv_id":null,"evidence_quote":"Uses MILP and counterexample guidance to learn from positive examples only, grounding the positive-only setting."},{"cited_title":"Exact synthesis of LTL properties from traces","cited_arxiv_id":null,"evidence_quote":"Adds strongness as an optimization criterion and uses counterexample-guided SAT search, completing the positive-only comparison."},{"cited_title":"Specification: The biggest bottleneck in formal methods and autonomy","cited_arxiv_id":null,"evidence_quote":"GPU-accelerated enumeration with relaxed unique checks and divide-and-conquer supports the scalability claims for enumeration-based methods."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"A graph-neural-network approach with a faithful LTL encoding, showing reliable formula extraction from trained networks."}],"review_version":1}