{"id":"ae17b039-e329-466d-8c22-39b97e331978","arxiv_id":"1908.04645","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"LTL can be translated to self-loop alternating automata with Emerson-Lei acceptance using F and G state-merging, yielding smaller automata than traditional Büchi/co-Büchi SLAA.","lead":"This paper presents new translations between linear temporal logic (LTL) and self-loop alternating automata (SLAA) that use a more expressive acceptance condition, Emerson-Lei acceptance. The result is a translation producing considerably smaller automata for formulas with F and G operators, and a proof that the automata class has the same expressive power as LTL.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 1's proof leans on the unproved synchronization Proposition 1; its extension to infinitely many runs in the G-case is especially fragile.","rationale":"The reader's weakest-assumption analysis identifies exactly the same load-bearing concern: the correctness proof of Theorem 1 invokes Proposition 1 as a black box, and the proposition is nontrivial and unproved. I read the construction in detail and found no other flaw that is more central. The linear-state claim is plausible because the DNF blowup in F-merging is absorbed by acceptance marks and transitions, not by states; the back-translation sketch is concise but its claims are standard fixpoint-style reasoning and less risky. The experimental section is supported by a published implementation and reproducible scripts. The one step that would invalidate the main theorem if wrong is the synchronization lemma, and the manuscript provides no proof or reference for it. Since no counterexample or concrete error was found, a conditional verdict is appropriate rather than rejection. If a proof of Proposition 1 is supplied, or a counterexample is shown not to exist, the paper would be much stronger; if a counterexample is found, the F,G-merging correctness proof would need substantial revision.","tokens_in":19194,"tokens_out":20155,"duration_ms":229663,"concrete_test":"Settle Proposition 1 by one of two checks. (1) Provide a complete proof of Proposition 1, including the infinite-run version used in the G-case; a natural route is induction on run DAGs showing that overlapping state occurrences can be fused by taking one of the two accepting continuations, relying on the suffix-closure of SLAA acceptance. (2) Search for a counterexample: exhaustively enumerate small SLAA with at most 3 states, at most 2 acceptance marks, and a 2-letter alphabet, and for every pair of suffixes of short words both in L(A), test whether accepting runs can be chosen synchronized. If any counterexample exists, the proof of Theorem 1 is invalid as written. A complementary machine-checked test is to formalize the G-case construction in Isabelle/HOL with Proposition 1 as an explicit axiom and check that the infinite family of runs used there is well-defined.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central correctness argument for the F,G-merging translation (Theorem 1, Appendix A) depends on Proposition 1, which asserts that accepting runs over suffixes of the same word can always be chosen mutually synchronized, and that this extends to runs of different inductively built automata. The proposition is stated without proof and is used in every compositional case of the inclusion L(φ) ⊆ L(Aφ). In the G-case it is applied to infinitely many runs at once: one accepting run of Aψ over every suffix wi.. for every conjunct ψ, with all of them assumed synchronized. Synchronization is not a formal consequence of the definitions: a union of two runs is a valid multitransition only if no source state appears in both runs with different transitions at the same position, and the proof gives no argument that such conflicts can be avoided while preserving acceptance. If Proposition 1 fails, the constructed unions T_i in the U, F, and G cases are not guaranteed to be multitransitions, so the proof of Theorem 1 collapses. No concrete counterexample was found, and the proposition may be true, but as written it is a load-bearing unproved lemma, not a routine detail. The back-translation (Theorem 2) is also only sketched, but the primary risk is the synchronization lemma.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper considers self-loop alternating automata (SLAA) with transition-based Emerson-Lei acceptance and presents two main results. First, it gives a sequence of translations from LTL to SLAA: a baseline co-Büchi construction, an F-merging variant producing Inf-less SLAA, and an F,G-merging variant producing SLAA with mixed Fin/Inf acceptance; Theorem 1 claims that the final translation is correct, has linearly many states, and at most exponentially many acceptance marks. Second, it gives a back-translation from SLAA with Emerson-Lei acceptance to LTL (Theorem 2), establishing equal expressive power. The paper also defines transition dominance for EL acceptance and reports experiments with the LTL3TELA tool showing state reductions on mergeable formulae.","tokens_in":19407,"tokens_out":18407,"duration_ms":189898,"significance":"The contribution is potentially valuable: the F,G-merging construction is a parameter-free, implemented translation that exploits generic acceptance for smaller intermediate automata, and the experiments indicate substantial savings on F/G-heavy formula sets, including more deterministic and nonalternating automata. The authors also provide a Jupyter notebook with the benchmark data, which is a concrete reproducibility strength. However, the central correctness proofs are not yet watertight: the synchronization lemma (Proposition 1) is used as a black box and the back-translation proof is only sketched. The expressiveness equivalence and the empirical claims depend on these results, so the paper needs a revision that supplies the missing arguments.","major_comments":[{"comment":"Proposition 1 is stated without proof and is load-bearing: it is invoked to compose accepting runs of subformula automata in every case of the inclusion L(φ) ⊆ L(Aφ), and in the G-case it is applied to infinitely many runs simultaneously. As written, the proof gives no argument that two accepting runs over suffixes of the same word can always be chosen so that their unions at each position are valid multitransitions, nor that this extends to runs of different automata. If this lemma fails, the constructed T_i are not guaranteed to be multitransitions and the proof of Theorem 1 collapses. Please provide a full proof of Proposition 1, or replace it with an explicit coinductive composition argument.","section":"Appendix A, Proposition 1"},{"comment":"The proof of Theorem 2 is a single sentence saying the statement follows by induction. The construction of φ(s) uses nested U and G operators whose semantics depend on infinite behavior, and the induction over the partial order must verify that runs that leave s after finitely many self-loops satisfy φ1(s) while runs that never leave s satisfy φ2(s) ∧ φ3(s). This is not a routine detail for a result establishing expressiveness equivalence; please include the induction in the appendix.","section":"Section 7, Theorem 2"},{"comment":"In the G-case of the reverse inclusion, the runs σψ_i are defined by the equation σψ_i = {t}(Ti+1[C′_i]... ⊔ σψ_{i+1}), which is an infinite regress rather than a well-founded induction. The proof needs to justify that the ⊔ operation produces valid multitransitions and that the resulting infinite runs are accepting; otherwise the claim that each σψ_i is accepting is unsupported.","section":"Appendix A, G-case of L(Aφ) ⊆ L(φ)"}],"minor_comments":[{"comment":"The two different mark symbols for each U and F subformula (e.g., ψ and ψ, or Fψ and Fψ) are not visually distinguished in the text. Since the correctness of the acceptance clauses depends on which mark is placed on the U-loop and the F-tt-loop, please clarify the notation.","section":"Section 5"},{"comment":"The sentence 'no ϕ appears in the run, so both Fin_ϕ and Fin_K_ϕ for some K ∈ ψ holds' is imprecise: the acceptance clause for Fψ is a disjunction with Inf_{Fψ}, and the proof should explicitly exclude the Inf case.","section":"Appendix A, Fψ case"},{"comment":"The sentence 'Furter, the F-merging...' contains a typo ('Furter' should be 'Further').","section":"Section 8.3"},{"comment":"References [4] and [17] are marked 'To appear'; if the publication details are now available, please update them.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The main risk is Proposition 1. If it is false, the F,G-merging construction may not be correct for some formulae; I did not find a counterexample, but the proof as written is incomplete. I would recommend making the synchronization lemma a centerpiece of the revision and asking the authors to supply the missing proof before the paper is accepted. The back-translation proof should also be expanded, though it looks plausible."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. First, this is the first LTL-to-SLAA translation targeting transition-based Emerson-Lei acceptance, and the F-merging and F,G-merging constructions do produce smaller SLAA on F/G-heavy formulas — about 45% state savings on their randfg benchmark, with more deterministic and nonalternating outputs. Second, the correctness proof of the main theorem has a load-bearing hole: Proposition 1, which guarantees mutually synchronized accepting runs for suffixes and across different automata, is stated without proof. I could not find a counterexample, and the proposition may well be true, but as written it is not a routine detail. The stress-test note is right to flag that the G-case applies it to infinitely many runs at once, which is exactly where conflicts in multitransition unions would hide if they exist.\n\nWhat is actually new: the F-merging and F,G-merging transformations (including the Inf-less intermediate class), the SLAA-to-LTL back-translation for Emerson-Lei acceptance, and the generalized transition-dominance simplification. The experiments are honest, with published scripts and a notebook; the fact that the basic translation reproduces LTL3BA's numbers gives some confidence the implementation is not drifting. The citation pattern is appropriate, and the self-citations are grounded in released tools.\n\nThe soft spots, in proportion. Proposition 1 is the main one; the paper's central Theorem 1 leans on it, and the appendix only asserts it. Theorem 2's 'straightforward by induction' is a sketch, but that back-translation looks more standard and the risk is lower. The DNF decomposition for F-subformulae can blow up the number of acceptance marks; they acknowledge this and state the exponential bound, so it is a cost, not a hidden flaw. The experimental comparison is on random formulas plus a small literature set, and the headline 45% saving comes from a benchmark biased toward F and G, so I would not generalize too far.\n\nWho this is for: anyone building LTL-to-automata pipelines or studying alternating automata with Emerson-Lei acceptance. It deserves a serious referee rather than a desk rejection. The right outcome is major revision: turn Proposition 1 into a real lemma with a proof (or weaken it to what the composition arguments actually need), and expand the proof of Theorem 2. I would not reject it on the current evidence.","headline":"Genuinely new LTL-to-SLAA translation work with real practical gains, but the main correctness proof has a load-bearing unproved lemma (Proposition 1) that a serious referee must ask to be fixed.","tokens_in":19970,"tokens_out":1589,"would_cite":true,"duration_ms":16189,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B44","68Q45","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Every LTL formula translates into a self-loop alternating automaton with mixed Fin/Inf acceptance, and the translation back to LTL is exact.","keywords":["linear temporal logic","self-loop alternating automata","Emerson-Lei acceptance","infinite words","automata translation","verification","acceptance conditions","state merging"],"falsifier":"Enumerate all LTL formulas up to some fixed size, build the F,G-merging automaton for each, and test language equivalence against a reference translator: any mismatch falsifies Theorem 1. A more surgical test is to search for a word with two suffixes each accepted by some SLAA but with no pair of accepting runs whose transitions can be synchronized, which would refute Proposition 1 and the induction that carries the proof.","tokens_in":1627,"feed_emoji":"🔄","tokens_out":2074,"duration_ms":92991,"temperature":0.7,"pith_summary":"Self-loop alternating automata (SLAA) are standard intermediates in translating linear temporal logic into automata that verification tools can use; previously they always used Büchi or co-Büchi acceptance. This paper shows that switching to a generic Emerson-Lei acceptance condition — a positive boolean combination of \"this mark appears finitely often\" and \"this mark appears infinitely often\" — makes the intermediate automata considerably smaller at no cost in language. Theorem 1 proves that the F,G-merging translation produces an equivalent SLAA with linearly many states, and Theorem 2 proves the reverse translation from any SLAA back to LTL is exact. The practical payoff is that F- and G-rich formulas, common in verification, produce automata with up to 45% fewer states, and many more of them are deterministic or purely existential.","feed_headline":"Merging F and G states shrinks LTL automata by up to 45%","feed_subtitle":"Mixed acceptance and state merging keep LTL semantics while shrinking the automata.","key_machinery":"The load-bearing object is the F,G-merging construction itself: for subformulas $F\\psi$, it expands $\\psi$ into disjunctive normal form over temporal formulas and merges the state $F\\psi$ with the resulting states $\\psi_K$; for subformulas $G\\bigwedge_i \\psi_i$, it merges $G\\psi$ with its conjunct states. The move that makes correctness work is the use of acceptance marks to track escaping multitransitions: a transition that leaves a merged state is marked, and the acceptance formula such as $\\mathrm{Fin}_\\psi \\lor \\mathrm{Inf}_\\psi$ for each $U$-subformula accepts a branch exactly when it would have been accepted under the unmerged translation. The proof relies on Proposition 1, which lets accepting runs over suffixes of one word be synchronized into a single run, and on the observation that a mark with a single owner is satisfied finitely-often exactly when either the mark appears finitely often or the owner state is escaped infinitely often.","core_discovery":"The paper's central claim is that the self-loop restriction of alternating automata does not force Büchi or co-Büchi acceptance. Its F,G-merging translation builds, for every LTL formula $\\varphi$, an SLAA $A_\\varphi$ whose language is exactly $L(\\varphi)$; the automaton has one state per subformula, so $O(|\\varphi|)$ states, and an acceptance condition that may use both Fin and Inf marks, with at most exponentially many marks. The translation merges the state for $F\\psi$ with states for the temporal disjuncts of $\\psi$, and merges $G\\psi$ with the states for its conjuncts, adjusting the acceptance formula with marks that record escaping multitransitions. The same expressive power is established by an explicit translation of any SLAA back to an equivalent LTL formula. The empirical claim, supported by measurements on literature and randomly generated formulas, is that these merged automata are often much smaller — over 45% fewer states in the F/G-heavy benchmark — and are more often deterministic or nonalternating.","pith_inferences":["The merging trick is asymmetric: it uses DNF for F and CNF for G, so a dual construction that merges $G\\psi$ with disjunctive components, or $F\\psi$ with conjunctive normal forms, might close the remaining gap and shrink automata for formulas the current rules cannot touch.","The single-owner observation behind the escaping-mark argument is general; any temporal operator whose semantics can be expressed by \"eventually, and then always\" style conditions may be mergeable by the same discipline of re-marking escaping transitions.","Because realistic verification specifications are rich in F and G patterns, the 45% savings on random F/G-heavy formulas likely understates the practical benefit on engineered specifications; this is a testable prediction against industrial pattern benchmarks.","Composing the forward and backward translations gives an LTL-to-LTL normalization that, combined with the smaller automata, may be useful for formula simplification outside automaton construction."],"forward_implications":["Every LTL formula now has an equivalent SLAA with transition-based Emerson-Lei acceptance, and conversely every such SLAA has an equivalent LTL formula; the two formalisms have the same expressive power.","The F,G-merging forward translation keeps the state count linear in formula size and bounds the number of acceptance marks exponentially, so it is asymptotically no worse than traditional Büchi or co-Büchi translations while offering better constants.","On formulas dominated by F and G operators, the construction saves over 45% of states on random benchmarks and turns many alternating automata into deterministic or purely existential ones.","Because the back-translation is exact, SLAA can be used as a lossless intermediate in pipelines that translate LTL to deterministic or nondeterministic automata.","The transition-dominance simplification extends to arbitrary Emerson-Lei acceptance, so smaller automata do not have to sacrifice post-construction simplification."],"supporting_citations":[{"why":"Supplies the definition of self-loop alternating automata and the survey of prior LTL-to-SLAA translations that the new construction improves.","marker":"[26]"},{"why":"Provides the basic LTL-to-SLAA construction and the transition-dominance simplification that the paper generalizes to Emerson-Lei acceptance.","marker":"[12]"},{"why":"Gives the previous state-of-the-art LTL-to-SLAA translation and simplification used as the experimental baseline.","marker":"[3]"},{"why":"Introduces the generic Emerson-Lei acceptance condition that the paper adopts for SLAA.","marker":"[10]"},{"why":"Reintroduces Emerson-Lei acceptance for transition-based automata in the HOA format, setting the practical context.","marker":"[1]"},{"why":"Defines the LTL syntax and semantics that the translations are proved equivalent to.","marker":"[22]"}],"fun_headline_variants":["New translation merges F/G, cuts LTL automata up to 45%","Self-loop automata: merged F/G states shrink LTL up to 45%","Merging F and G states: smaller LTL automata, up to 45%","Skip Buchi: F/G merging shrinks LTL automata up to 45%"],"cache_read_input_tokens":22144,"weakest_assumption_plain":"Everything in the correctness proof rests on Proposition 1, stated without proof in the appendix: any two accepting runs of an SLAA over suffixes of the same word can be chosen so their transitions line up into a single valid run, and if that fails the language-equality argument collapses.","fun_headline_variants_meta":{"raw":{"variants":["New translation merges F/G, cuts LTL automata up to 45%","Self-loop automata: merged F/G states shrink LTL up to 45%","Merging F and G states: smaller LTL automata, up to 45%","Skip Buchi: F/G merging shrinks LTL automata up to 45%"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001479,"raw_usage":{"total_tokens":5905,"prompt_tokens":868,"completion_tokens":5037,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":484,"completion_tokens_details":{"reasoning_tokens":4943}},"tokens_in":484,"tokens_out":5037,"duration_ms":37026,"temperature":1.0,"reasoning_tokens":4943,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:36:44.997945+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Enumerate all LTL formulas up to some fixed size, build the F,G-merging automaton for each, and test language equivalence against a reference translator: any mismatch falsifies Theorem 1. A more surgical test is to search for a word with two suffixes each accepted by some SLAA but with no pair of accepting runs whose transitions can be synchronized, which would refute Proposition 1 and the induction that carries the proof.","supporting_citations":[{"cited_title":"Automata and Linear Temporal Logic: Translat ions with Transition-Based Acceptance","cited_arxiv_id":null,"evidence_quote":"Supplies the definition of self-loop alternating automata and the survey of prior LTL-to-SLAA translations that the new construction improves."},{"cited_title":"Fast LTL to B¨ uchi Automata Transla tion","cited_arxiv_id":null,"evidence_quote":"Provides the basic LTL-to-SLAA construction and the transition-dominance simplification that the paper generalizes to Emerson-Lei acceptance."},{"cited_title":"LTL to B¨ uchi Au- tomata Translation: Fast and More Deterministic","cited_arxiv_id":null,"evidence_quote":"Gives the previous state-of-the-art LTL-to-SLAA translation and simplification used as the experimental baseline."},{"cited_title":"Modalities for Model Checking: Bra nch- ing Time Logic Strikes Back","cited_arxiv_id":null,"evidence_quote":"Introduces the generic Emerson-Lei acceptance condition that the paper adopts for SLAA."},{"cited_title":"The Hanoi Omega-Automata Forma t","cited_arxiv_id":null,"evidence_quote":"Reintroduces Emerson-Lei acceptance for transition-based automata in the HOA format, setting the practical context."},{"cited_title":"The Temporal Logic of Programs","cited_arxiv_id":null,"evidence_quote":"Defines the LTL syntax and semantics that the translations are proved equivalent to."}],"review_version":1}