Characterizing the Polynomial-Time Minimizable $\omega$-Automata

Bader Abu Radi; R\"udiger Ehlers

REVIEW

Characterizing the Polynomial-Time Minimizable $\omega$-Automata

Bader Abu Radi, Rüdiger Ehlers

Formal Languages and Automata Theory · Submitted 29 Apr 2025 · 29 references

Pith's verdict: Strong paper that closes the two remaining open minimization cases; the only real flaw is a sign slip in Proposition 13's language equality, which is easily fixed and does not threaten the theorem.

T0 · AI review

How this review was made: An AI referee (deepseek-v4-flash) read the paper on August 16, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

T0 AI review An AI read the paper and answered a fixed list of questions.
T1 Audit Automatic checks that the references and files the paper relies on exist and match.
T2 Compute The paper's code or calculations re-run with the same results.
T3 Formal statement The claims written out in a formal math language a computer can read.
T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· 1 major objection · 4 minor · Ask about this paper · The compiled record · Read the full review →

Challenge this review Comment (0) Read on arXiv ↗

Cite ▾

arXiv ID2504.20553 (version 1)

Pith IDOM3N6DLI, Pith's permanent record of this paper and its review

CitationBader Abu Radi, R\"udiger Ehlers. "Characterizing the Polynomial-Time Minimizable $\omega$-Automata." arXiv:2504.20553 (2025). https://pith.science/paper/OM3N6DLI

Cite this reviewBibTeX for Pith's review of this paper

Claim paper

Why Pith says this

Highlight any text to comment on it.

Editor's note

read the letter

Bottom line: this paper is the real thing. It closes the last two open cells in the minimization complexity table for deterministic and history-deterministic automata with transition-based acceptance, and the main reduction is worked out in serious detail. The reader's ACCEPT verdict is right, with one caveat.

The genuinely new results are NP-hardness for tDCW minimization and for HD-tNBW minimization with transition-based acceptance. The route through a restricted Hamiltonian path problem, the construction of a minimal HD-tNCW whose deterministic equivalent exists exactly when the path exists, and the polynomial-alphabet encoding are all substantive. The appendices are long but the arguments are mostly self-contained, and the reliance on [1] and [3] is legitimate: those are published external theorems, not the target claim. The paper earns credit for spelling out the chain rather than hand-waving.

The soft spot is Proposition 13. As printed, the proof writes L(C)=L(B)=L(e(AGv1p))=L(e(AGv1)). That first equality is not what [3] gives. [3] complements an HD-tNBW, so the HD-tNCW C should recognize the complement of L(B), which is L(e(AGv1p)), not L(B) itself. With that sign corrected, the inequalities |e(AGv1)|≤|C|≤|B|≤|e(AGv1)| force equality and the transfer to HD-tNBW and tDBW hardness goes through. So this is a genuine slip in the write-up, but a cosmetic one; the intended argument is sound.

Two smaller things. First, the polynomial alphabet encoding in Appendix E is intricate, and I did not re-verify every internal state and transition by hand. It looks careful, but it is the part most likely to harbor a subtle error, so a referee should spend time there. Second, the related-work attribution in Table 1 is sometimes indirect, but the discussion in Appendix A handles that reasonably.

Who is this for? Automata theorists working on minimization, history-determinism, or the complexity of omega-automata. It deserves a serious referee, and I would be happy to see it in a good venue after the Proposition 13 equality is fixed.

Referee report

Significance

If the proofs are correct, this is a substantial contribution: it resolves several previously open minimization problems, establishes NP-completeness for classes where only partial information was known, and completes the complexity landscape for the branching modes and acceptance conditions considered. The reduction construction is intricate and original, especially the use of safe-component memories to encode Hamiltonian paths, and the appendices contain a serious amount of proof detail. A notable strength is that the main construction is not merely stated but carried through the encodings e(AGv1) and e(AGv1p), including explicit proofs that the encodings preserve minimality, language equivalence, and determinism. The paper does not ship machine-checked proofs or code, and the correctness of the hardness transfers depends on two external structural theorems, [1, Theorem 17] and [3]; both dependencies are explicitly disclosed. The central flaw I found is a complementation sign error in Section 5, Proposition 13.

Major objections (1)

[Section 5, Proposition 13] The proof of Proposition 13 contains a complementation sign error that is load-bearing for the HD-tNBW and tDBW hardness transfer. The reduction constructs the tDBW ^e(AGv1p), so the assumption is L(B) = L(^e(AGv1p)), i.e., B recognizes the complement of L(e(AGv1p)). The cited result [3] produces an HD-tNCW for the complement of an HD-tNBW, so the displayed chain "L(C) = L(B) = L(e(AGv1p)) = L(e(AGv1))" is not correct: it asserts L(B) = L(e(AGv1p)), which contradicts the assumption. The intended chain is L(C) = complement(L(B)) = L(e(AGv1p)) = L(e(AGv1)). With that correction, the inequalities |e(AGv1)| ≤ |C| ≤ |B| ≤ |e(AGv1)| force equality and Qdet = QB, and the rest of the argument goes through. As printed, however, the proof of Proposition 13 does not establish the claimed transfer to HD-tNBW and tDBW. The same sign error appears in the notation paragraph above Proposition 13, where the dual of a tDBW A is described as satisfying L(A) = L(~A); the correct statement is L(~A) = complement(L(A)).

Minor objections (4)

[Appendix E, Example 29] The text refers to Figure 1 when describing the encoding e(AGv1), but no figure appears in the submitted manuscript. The example is difficult to follow without that figure; either include it or remove the reference.
[Appendix D.3, Lemma 24] The proof of Lemma 24 overloads the name z1: it is first defined as the four-letter word (AP)^4, and later the same name is used for a five-letter extension z1 = σ1·σ2·σ3·σ4·σ5. Renaming the extension would avoid confusion.
[Throughout] There are several typographical errors: "determinstic" in Section 3, "acecptance" in Section 6, "benifit" in Section 6, "polynomialy" in Section 5, and "a a Hamiltonian path" in the proof of Proposition 13. These should be corrected in a revision.
[Section 5, paragraph before Proposition 13] The definitions of the dual automata ~A for tDBW and tDCW are stated asymmetrically and, for tDBW, incorrectly. The sentence "The Büchi and co-Büchi acceptance conditions are dual in the sense that L(A) = L(~A)" should be replaced by a complement relation.

How Pith checks papers → · Full audit of this paper →

The paper

The paper claims

The paper proves that minimizing transition-based deterministic co-Büchi and history-deterministic Büchi automata is NP-complete, completing the complexity map for polynomial-time minimizable ω-automata.

The reading

The paper closes the remaining open cases in the complexity of minimizing automata over infinite words. It proves that minimizing deterministic transition-based co-Büchi automata, deterministic transition-based Büchi automata, and history-deterministic transition-based Büchi automata is NP-complete. The proof encodes a restricted Hamiltonian path problem into a minimal history-deterministic co-Büchi automaton whose state count can be matched by a deterministic automaton exactly when a Hamiltonian path exists. If the paper is correct, polynomial-time minimization survives only for history-deterministic transition-based co-Büchi automata, and no polynomial-time minimizer exists for the other classes unless P equals NP.

What carries the argument

The load-bearing construction is a family of safe components, one for each graph vertex, plus a special synchronizing component SSync. Each safe component traps infinite words whose suffix satisfies a local consistency language Lv, using states that store the past-one and past-two values of neighboring vertices. The synchronizing component SSync traps words with regular sleep-letter spacing and an extra-consistency condition linking the current letter to the past value of v1. Deterministic pruning of AGv1 must jump between safe components only along graph edges, so matching the minimal state count forces the automaton to trace a Hamiltonian path. To make the alphabet polynomial, the paper encodes letters as binary strings and keeps internal states only for atomic propositions that are essential to a state; bounded degree ensures only constantly many propositions matter, so the encoded automaton e(AGv1) remains polynomial in the graph size and preserves the same equivalence.

Extended reading notes

Core claim

The central claim is Theorem 14: for each of the classes tDBW, tDCW, and HD-tNBW, the minimization problem—given an automaton and a bound k, decide whether an equivalent automaton with at most k states exists—is NP-complete. The proof reduces from a bounded-degree Hamiltonian path variant. A graph G is transformed into a minimal HD-tNCW AGv1 whose safe components encode the graph's vertices and whose synchronizing safe component SSync enforces timing and memory constraints. The automaton AGv1 has a deterministic equivalent of the same size if and only if G has a Hamiltonian path starting at a fixed vertex v1. Because every graph also admits a polynomially larger deterministic tDCW AGv1p obtained by duplicating safe components along a path that visits all vertices, any polynomial-time minimizer for tDCWs could be used to detect Hamiltonian paths, giving NP-hardness. Duality transfers the result to tDBWs, and a complementation property of HD-tNBWs transfers it to history-deterministic Büchi automata.

Load-bearing premise

The hardness proof assumes the canonical-structure theorem that minimal equivalent history-deterministic transition-based co-Büchi automata with well-behaved safe components have isomorphic safe components and matching safe languages; this is what lets the argument read a Hamiltonian path off an arbitrary deterministic minimizer rather than off a specially constructed one.

Editorial extensions

If this is right

The decision version of minimizing tDCW, tDBW, and HD-tNBW is NP-complete: with k as part of the input, no polynomial algorithm can decide whether an equivalent automaton with at most k states exists unless P=NP.
Within the deterministic and history-deterministic automata over infinite words, polynomial-time minimization survives only for history-deterministic transition-based co-Büchi automata (assuming P≠NP); the combination of history-determinism, transition-based acceptance, and co-Büchi acceptance is exactly the polynomial-time region.
The HD-negativity problem—deciding whether a minimal HD-tNCW admits an equally small deterministic co-Büchi automaton—is NP-hard, so history-determinism genuinely saves states for co-Büchi languages in general.
The restricted Hamiltonian path problem, with a designated start vertex and bounded degree, can be encoded in polynomially many automaton states over a polynomial alphabet, so the hardness persists for realistically sized automata rather than only for exponentially large alphabets.
Deterministic Büchi minimization is NP-hard by duality from the co-Büchi result, completing the complexity table for all combinations of branching mode, Büchi/co-Büchi acceptance, and state-based or transition-based acceptance.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the dichotomy holds, practical automata-minimization tools for reactive synthesis should concentrate on history-deterministic transition-based co-Büchi automata and on chain-of-co-Büchi decompositions; the paper gestures at this conclusion but does not develop it as a tooling recommendation.
The same safe-component encoding may transfer to other automaton families whose canonical minimization requires reading a Hamiltonian path from a deterministic pruning, suggesting a general template for NP-hardness beyond the specific classes treated here.
A checkable extension is whether the hardness survives when the input graphs have bounded treewidth: Hamiltonian path is tractable there, so if the reduction's automata become minimizable in polynomial time on those graphs, the source of hardness is fully located in the graph problem.
The paper's framing implies that transition-based acceptance is not merely a factor-2 syntactic convenience: even though transition-based automata compress state-based automata by at most a factor of 2, the transition-based minimization problem itself is NP-hard, so that factor cannot be leveraged into a polynomial-time approximation algorithm.

Original abstract

A central question in the theory of automata is which classes of automata can be minimized in polynomial time. We close the remaining gaps for deterministic and history-deterministic automata over infinite words by proving that deterministic co-B\"uchi automata with transition-based acceptance are NP-hard to minimize, as are history-deterministic B\"uchi automata with transition-based acceptance.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13.0 via TypeSafe API, question bank abstract-p1-20260923, 2026-09-23: 1 request, 2,316 input tokens.

What the abstract itself states, as probabilities: claims first 0.09 · states limitation 0.31 · human participants 0.01 · controlled comparison 0.02 · randomized assignment 0.01 · states quantitative result 0.36 · compares with prior results 0.33 · mentions code or data availability 0.02.

The abstract, sentence by sentence

arXiv listing abstract v1. Results and the main claim are underlined; show every role.

A central question in the theory of automata is which classes of automata can be minimized in polynomial time. We close the remaining gaps for deterministic and history-deterministic automata over infinite words by proving that deterministic co-B\"uchi automata with transition-based acceptance are NP-hard to minimize, as are history-deterministic B\"uchi automata with transition-based acceptance.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#	sentence	role	the authors' own work	states the main conclusion	strength
s0	A central question in the theory of automata is which classes of automata can be minimized in polynomial time.	background 1.00	0.04	0.03	asserted 0.54
s1	We close the remaining gaps for deterministic and history-deterministic automata over infinite words by proving that deterministic co-B\"uchi automata with transition-based acceptance are NP-hard to minimize, as are history-deterministic B\"uchi automata with transition-based acceptance.	result 0.77	0.94	0.93	asserted 1.00

What kind of paper the classifier reports this is: theoretical result 1.00 · evidence from proof or derivation 1.00.

What was examined, and what was not

sources read

arXiv listing abstract v1

not examined

full text
figures and tables
references and citing sentences
relations to other papers

levels run

P abstract

not run

S sections
T body sentences
C citations
R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

References

Works cited (29)

[1]

Either the finite runp can be extended to a run onw by appending an infinite safe run pi,pi+1,... on the suffixw[i + 1,∞]. In this case, asA is safe-deterministic and alpha- homogeneous, we get thatpi,pi+1,... is the only run frompi on the suffixw[i + 1,∞], and so there is a unique extension ofp

View on Pith
[3]

The stater4 is a state inS(v1), yet does not encode the correct past values with respect toz1: we can follow the proof sketch of item 2 but with a careful modification to theextra 30 Characterizing the Polynomial-Time Minimizable ω-Automata values in some letters while (possibly) introducing an additional safe transition along the extended runr. Specifica...

View on Pith
[2]

Or, the finite runp cannot be extended to a run onw by appending a safe runpi,pi+1,... on the suffixw[i + 1,∞]. In this case, consider the minimalj≥i such thatpi w[i+1,j] −−−−−→pj is a safe run and the statepj has no safew[j + 1]-labeled transition. Then, asr[i,∞] is a safe run on the suffixw[i+1,∞], it follows that for allk>j , the runr[0,k ] =r0,r 1,......

View on Pith
[4]

Consider a stateq∈ Q ofAGv1 . Then, it holds thatL(q) is the language of infinite wordsw having a suffix inLSync or a suffix that is a mix of(sleep)ω and some word in (⋃ v∈V Lv). In particular, all the states ofAGv1 are language-equivalent. Proof. 1. Immediate from the definition ofAGv1

View on Pith
[5]

We start with the easy direction, namely, showing that every infinite wordw =σ1·σ2··· in L(q) has a suffix inLSync or a suffix that is a mix of(sleep)ω and some word in (⋃ v∈V Lv). Letr =r0,r 1,r 2,... be an accepting run ofq on w. Asr is accepting, there is somei≥ 0 such that the runr[i,∞] = ri,ri+1,ri+2,... is a safe run on the suffix w[i + 1,∞]. Either...

View on Pith
[6]

The transitiont =⟨s0,σ 1,s 1⟩ is extra-consistent andv1∈σ1, or

View on Pith
[7]

S(s0) =S(v) for some vertexv̸=v1, and{v1, extra}⊆ σ1. then the runr enters the safe componentSSync. Proof. As the transitiont =⟨s0,σ 1,s 1⟩ is rejecting, then, by Lemma 21, it is sufficient to show the existence of a finite nonempty wordy such that (σ1··· σk·y)ω is extra-consistent and rc =s0 σ1 −→s1 σ2·σ3···σk −−−−−−→sk y − →s0 is a cycle inAd that ends ...

View on Pith
[8]

The transitiont =⟨s0,σ 1,s 1⟩ is extra-consistent, andv1∈ σ1: as t is extra-consistent, then s0∈S (v1). Letps0 1 (v1) denote the encoded past-one value ofv1 in the states0. As S(s0) =S(sk) =S(v1), then there is a finite safe runr′ from sk to s0 inS(v1) labeled with some finite nonempty wordy =y1·y2··· ym over 2AP. Indeed, the safe component S(v1) is non-t...

View on Pith
[9]

S(s0) =S(v) for some vertexv̸= v1, and{v1, extra}⊆ σ1: as v̸= v1, andv1 has no incoming edges inG, we have thatS(v) does not track past values ofv1. In particular, if r′ =sk y1·y2···ym −−−−−−→s0 is a safe run fromsk to s0 insideS(v) over a nonempty word in (2AP)∗, then we can assume w.l.o.g that every letter ofy containsv1 and extra. Then, it is not hard ...

View on Pith
[10]

v =v1, v1∈σ and the transitiont =⟨s−1,σ,s⟩ is extra-consistent, or

View on Pith
[11]

v̸=v1 and{v1, extra}⊆ σ, then there is a nonempty finite wordwq such that the run ofAq d on wq is safe, yet the run of As d on wq entersSSync for the first time upon reading the last letter ofwq. Proof. We first show the existence of a nonempty finite wordx1 such that every letter of x1 contains v1 and extra, the run ofq on x1 is safe, yet the run ofs on ...

View on Pith
[12]

The stater4 = (t,k ) is inSSync: consider the runr′ ofA(1,1) d on z1· sleep. The run r′ = (1, 1) AP −−→(2, 1) AP −−→(3, 1) AP −−→(4, 1) AP −−→(t,k ) sleep −−−→(1,k ) is a non-safe run from the state (1, 1) to the state (1,k ). We distinguish between two cases. Either k = 1 or k = 0. If k = 1, we get thatr′ is a non-safe cycle from (1, 1) labeled with the ...

View on Pith
[13]

reduces the non-acceptance of a polynomially-spaced Turing machine to the universality problem of an automaton. The word to be accepted is encoded into the input of the automaton. The construction can be altered so that once an accepting state of the Turing machine is reached, the run of the automaton ends, so that the corresponding run can only be accept...

View on Pith
[14]

The stater4 is a state inS(v) for some vertexv̸= v1: let η(v) ={v,u 1,u 2,...,u m} denote the neighborhood ofv, letr4 = [p1(u1),p 1(u2),...,p 1(um),p 1(v),p 2(v),v ], and let z1 =σ1·σ2·σ3·σ4 = (AP)4. Now ifp2(v) = 1, then we modify the letterσ3 in z1 to σ3 = AP\{v}. Thus, we modifiedσ3 so that the runr enters a stater4 that does not remember the correct p...

View on Pith
[15]

S(s1) = S(v1), for all j ∈{ 2, 3,...,i },S(sj) = S(vj) for some vertexvj, and p = (v1,v 2,...,v i) is a simple path inG

View on Pith
[16]

For allj∈ [i], the runrz entersS(vj) once upon reading the last letter ofzj by moving to the statesj that encodes the correct past values of every vertex inη(vj) with respect to the prefixz1·z2··· zj. In addition,rz stays in the same safe component while reading the infix zj[1,|zj|− 1]

View on Pith
[17]

For every vertexu∈V\{v1,v 2,...,v i}, the wordz can be extended to an infinite word in Lu. In addition, every letter inz containsv1 and extra. Bader Abu Radi and Rüdiger Ehlers 31 If p is not a Hamiltonian-path, then there is a wordzi+1 such that every letter inzi+1 containsv1 and extra, and the runr ofAsi d on zi+1 leavesS(si) and enters a statesi+1 upon...

View on Pith
[18]

There is a vertexvi+1∈V\{v1,v 2,...,v i} such that¬E(vi,vi+1) and si+1∈S (vi+1): First, recall the extended runrz = (1, 1) z1 −→s1 z2 −→s2··· zi −→si σl+1 −−−→s σl+2 −−−→si+1 that is defined over the wordz1·z2··· zi·zi+1 = σ1·σ2······ σl·σl+1·σl+2 starting with z1 = ( AP)4. As ¬E(vi,vi+1), then the safe componentS(si) = S(vi) does not track past values of...

View on Pith
[19]

There is a vertexvi+1∈V\{v1,v 2,...,v i} such thatE(vi,vi+1) and si+1∈S (vi+1), yet the statesi+1 does not encode the correct past values with respect toz1·z2··· zi·zi+1: First, recall the extended runrz = (1, 1) z1 −→s1 z2 −→s2··· zi −→si σl+1 −−−→s σl+2 −−−→si+1. We define the letterσl+3 = V∪{ extra}∪{ ˆ v: v∈ V∩σl+2}∪{ ˇ v| v∈ V∩σl+1} = V∪{ extra}∪{ ˆ ...

View on Pith
[20]

The state si+1 belongs to the safe component SSync: Since the simple path p = (v1,v 2,...,v i) is not Hamiltonian, then there is a vertexv /∈ {v1,v 2,...,v i}. Con- sider the extended runrz = (1, 1) z1 −→s1 z2 −→s2··· zi −→si zi+1 −−−→si+1, and recall that z1 = (AP)4, andz′ =z1·z2··· zi··· zi+1 can be extended to an infinite word inLv. Then, let vec z′ −→...

View on Pith
[21]

The state si+1 belongs to the safe componentS(sj) for some j ∈ [i]: the run rz = (1, 1) z1 −→s1 z2 −→s2··· zi −→si zi+1 −−−→si+1 is such thatsj zj+1 −−−→··· zi −→si zi+1 −−−→si+1 is a non-safe run that does not visitSSync, and starts and ends in the same safe component. To reach a contradiction, we show that the latter run can be extended to a non-safe cy...

View on Pith
[22]

q∈S (v) for some vertexv∈ V and ai = v′ for somev′ vertex withd(v,v′)≤ 2, or ai = ˆv′ for some vertexv′ with d(v,v′) = 1, orai = ˇv. Thus,ai corresponds to the values of vertices of distance at most2 from v, or the hat values of neighbors ofv, or the check Bader Abu Radi and Rüdiger Ehlers 35 value ofv

View on Pith
[23]

q∈S (v) for some vertexv̸=v1 and ai =v1

View on Pith
[24]

q∈S Sync and ai = extra, orai∈V is a vertex withd(v1,ai)≤ 1. Thus,ai corresponds to the values of vertices in the neighborhood ofv1, or the value ofextra. ▶ Remark 27. Consider a stateq∈ Q, and an atomic propositionai∈ AP. When ai is essential toq, then the assignment ofai is essential not only for determining safe transitions insideAGv1 , but also for de...

View on Pith
[25]

All runs of(e(AGv1 ))s on⟨σ⟩ end in a state inQ. In addition, if a runr =s ⟨σ⟩ −−→p exists in e(AGv1 ), then it is unique, and is of the formr =s,s⟨σ⟩[1,1],s⟨σ⟩[1,2],...,s ⟨σ⟩[1,k−1],p. 38 Characterizing the Polynomial-Time Minimizable ω-Automata

View on Pith
[26]

The triple⟨s,σ,p⟩ is a transition ofAGv1 iff there is a runr =s ⟨σ⟩ −−→p in e(AGv1 ). In addition, the runr is safe only when the transition⟨s,σ,p⟩ is safe. Proof. 1. Is immediate from the definition ofe(AGv1 ). Indeed, upon reading⟨σ⟩ from s, we move deterministically via safe transitions to the states⟨σ⟩[1,i] after reading thei’th bit of⟨σ⟩ for alli∈ [k...

View on Pith
[27]

Consider a triplet =⟨s,σ,p⟩∈ Q× Σ×Q. By the definition ofe(AGv1 ), we know that there is a safe run of the forms ⟨σ⟩[1,k−1] −−−−−−→s⟨σ⟩[1,k−1] in e(AGv1 ). In addition, the above run can be extended to a runr from s on⟨σ⟩ to p only when the triplet =⟨s,σ,p⟩ is a transition ofAGv1 . The definition of the acceptance condition ofe(AGv1 ) implies that the run...

View on Pith
[28]

The run of e(AGv1p )⟨s,i1⟩ on ⟨σ⟩ ends in a state in Qv1,p. In addition, if a run r = ⟨s,i 1⟩ ⟨σ⟩ −−→ ⟨q,i 2⟩ exists in e(AGv1p ), then it is unique, and is of the form r =⟨s,i 1⟩,⟨s⟨σ⟩[1,1],i 1⟩,⟨s⟨σ⟩[1,2],i 1⟩,..., ⟨s⟨σ⟩[1,k−1],i 1⟩,⟨q,i 2⟩

View on Pith
[29]

The triple⟨⟨s,i 1⟩,σ,⟨q,i 2⟩⟩ is a transition ofAGv1p iff there is a runr =⟨s,i 1⟩ ⟨σ⟩ −−→⟨q,i 2⟩ in e(AGv1p ). In addition, the runr is safe only when the transition⟨⟨s,i 1⟩,σ,⟨q,i 2⟩⟩ is safe. Proof. The proof is similar to that of Lemma 30 and is immediate from the definitions. Specifically, when reading⟨σ⟩ from⟨s,i 1⟩, we move deterministically to the...

View on Pith

How the literature uses it

2 arXiv papers cite this in 2 sentences

Each citing sentence is taken from the citing paper's LaTeX source and typed by Pith's classifier. A label appears at probability 0.8 or more (0.95 for support), a contest at 0.7 or more; the quoted words are the citing authors'. How each label was checked · JSON

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.

[1] [1]

Either the finite runp can be extended to a run onw by appending an infinite safe run pi,pi+1,... on the suffixw[i + 1,∞]. In this case, asA is safe-deterministic and alpha- homogeneous, we get thatpi,pi+1,... is the only run frompi on the suffixw[i + 1,∞], and so there is a unique extension ofp

View on Pith

[2] [3]

The stater4 is a state inS(v1), yet does not encode the correct past values with respect toz1: we can follow the proof sketch of item 2 but with a careful modification to theextra 30 Characterizing the Polynomial-Time Minimizable ω-Automata values in some letters while (possibly) introducing an additional safe transition along the extended runr. Specifica...

View on Pith

[3] [2]

Or, the finite runp cannot be extended to a run onw by appending a safe runpi,pi+1,... on the suffixw[i + 1,∞]. In this case, consider the minimalj≥i such thatpi w[i+1,j] −−−−−→pj is a safe run and the statepj has no safew[j + 1]-labeled transition. Then, asr[i,∞] is a safe run on the suffixw[i+1,∞], it follows that for allk>j , the runr[0,k ] =r0,r 1,......

View on Pith

[4] [4]

Consider a stateq∈ Q ofAGv1 . Then, it holds thatL(q) is the language of infinite wordsw having a suffix inLSync or a suffix that is a mix of(sleep)ω and some word in (⋃ v∈V Lv). In particular, all the states ofAGv1 are language-equivalent. Proof. 1. Immediate from the definition ofAGv1

View on Pith

[5] [5]

We start with the easy direction, namely, showing that every infinite wordw =σ1·σ2··· in L(q) has a suffix inLSync or a suffix that is a mix of(sleep)ω and some word in (⋃ v∈V Lv). Letr =r0,r 1,r 2,... be an accepting run ofq on w. Asr is accepting, there is somei≥ 0 such that the runr[i,∞] = ri,ri+1,ri+2,... is a safe run on the suffix w[i + 1,∞]. Either...

View on Pith

[6] [6]

The transitiont =⟨s0,σ 1,s 1⟩ is extra-consistent andv1∈σ1, or

View on Pith

[7] [7]

S(s0) =S(v) for some vertexv̸=v1, and{v1, extra}⊆ σ1. then the runr enters the safe componentSSync. Proof. As the transitiont =⟨s0,σ 1,s 1⟩ is rejecting, then, by Lemma 21, it is sufficient to show the existence of a finite nonempty wordy such that (σ1··· σk·y)ω is extra-consistent and rc =s0 σ1 −→s1 σ2·σ3···σk −−−−−−→sk y − →s0 is a cycle inAd that ends ...

View on Pith

[8] [8]

The transitiont =⟨s0,σ 1,s 1⟩ is extra-consistent, andv1∈ σ1: as t is extra-consistent, then s0∈S (v1). Letps0 1 (v1) denote the encoded past-one value ofv1 in the states0. As S(s0) =S(sk) =S(v1), then there is a finite safe runr′ from sk to s0 inS(v1) labeled with some finite nonempty wordy =y1·y2··· ym over 2AP. Indeed, the safe component S(v1) is non-t...

View on Pith

[9] [9]

S(s0) =S(v) for some vertexv̸= v1, and{v1, extra}⊆ σ1: as v̸= v1, andv1 has no incoming edges inG, we have thatS(v) does not track past values ofv1. In particular, if r′ =sk y1·y2···ym −−−−−−→s0 is a safe run fromsk to s0 insideS(v) over a nonempty word in (2AP)∗, then we can assume w.l.o.g that every letter ofy containsv1 and extra. Then, it is not hard ...

View on Pith

[10] [10]

v =v1, v1∈σ and the transitiont =⟨s−1,σ,s⟩ is extra-consistent, or

View on Pith

[11] [11]

v̸=v1 and{v1, extra}⊆ σ, then there is a nonempty finite wordwq such that the run ofAq d on wq is safe, yet the run of As d on wq entersSSync for the first time upon reading the last letter ofwq. Proof. We first show the existence of a nonempty finite wordx1 such that every letter of x1 contains v1 and extra, the run ofq on x1 is safe, yet the run ofs on ...

View on Pith

[12] [12]

The stater4 = (t,k ) is inSSync: consider the runr′ ofA(1,1) d on z1· sleep. The run r′ = (1, 1) AP −−→(2, 1) AP −−→(3, 1) AP −−→(4, 1) AP −−→(t,k ) sleep −−−→(1,k ) is a non-safe run from the state (1, 1) to the state (1,k ). We distinguish between two cases. Either k = 1 or k = 0. If k = 1, we get thatr′ is a non-safe cycle from (1, 1) labeled with the ...

View on Pith

[13] [13]

reduces the non-acceptance of a polynomially-spaced Turing machine to the universality problem of an automaton. The word to be accepted is encoded into the input of the automaton. The construction can be altered so that once an accepting state of the Turing machine is reached, the run of the automaton ends, so that the corresponding run can only be accept...

View on Pith

[14] [14]

The stater4 is a state inS(v) for some vertexv̸= v1: let η(v) ={v,u 1,u 2,...,u m} denote the neighborhood ofv, letr4 = [p1(u1),p 1(u2),...,p 1(um),p 1(v),p 2(v),v ], and let z1 =σ1·σ2·σ3·σ4 = (AP)4. Now ifp2(v) = 1, then we modify the letterσ3 in z1 to σ3 = AP\{v}. Thus, we modifiedσ3 so that the runr enters a stater4 that does not remember the correct p...

View on Pith

[15] [15]

S(s1) = S(v1), for all j ∈{ 2, 3,...,i },S(sj) = S(vj) for some vertexvj, and p = (v1,v 2,...,v i) is a simple path inG

View on Pith

[16] [16]

For allj∈ [i], the runrz entersS(vj) once upon reading the last letter ofzj by moving to the statesj that encodes the correct past values of every vertex inη(vj) with respect to the prefixz1·z2··· zj. In addition,rz stays in the same safe component while reading the infix zj[1,|zj|− 1]

View on Pith

[17] [17]

For every vertexu∈V\{v1,v 2,...,v i}, the wordz can be extended to an infinite word in Lu. In addition, every letter inz containsv1 and extra. Bader Abu Radi and Rüdiger Ehlers 31 If p is not a Hamiltonian-path, then there is a wordzi+1 such that every letter inzi+1 containsv1 and extra, and the runr ofAsi d on zi+1 leavesS(si) and enters a statesi+1 upon...

View on Pith

[18] [18]

There is a vertexvi+1∈V\{v1,v 2,...,v i} such that¬E(vi,vi+1) and si+1∈S (vi+1): First, recall the extended runrz = (1, 1) z1 −→s1 z2 −→s2··· zi −→si σl+1 −−−→s σl+2 −−−→si+1 that is defined over the wordz1·z2··· zi·zi+1 = σ1·σ2······ σl·σl+1·σl+2 starting with z1 = ( AP)4. As ¬E(vi,vi+1), then the safe componentS(si) = S(vi) does not track past values of...

View on Pith

[19] [19]

There is a vertexvi+1∈V\{v1,v 2,...,v i} such thatE(vi,vi+1) and si+1∈S (vi+1), yet the statesi+1 does not encode the correct past values with respect toz1·z2··· zi·zi+1: First, recall the extended runrz = (1, 1) z1 −→s1 z2 −→s2··· zi −→si σl+1 −−−→s σl+2 −−−→si+1. We define the letterσl+3 = V∪{ extra}∪{ ˆ v: v∈ V∩σl+2}∪{ ˇ v| v∈ V∩σl+1} = V∪{ extra}∪{ ˆ ...

View on Pith

[20] [20]

The state si+1 belongs to the safe component SSync: Since the simple path p = (v1,v 2,...,v i) is not Hamiltonian, then there is a vertexv /∈ {v1,v 2,...,v i}. Con- sider the extended runrz = (1, 1) z1 −→s1 z2 −→s2··· zi −→si zi+1 −−−→si+1, and recall that z1 = (AP)4, andz′ =z1·z2··· zi··· zi+1 can be extended to an infinite word inLv. Then, let vec z′ −→...

View on Pith

[21] [21]

The state si+1 belongs to the safe componentS(sj) for some j ∈ [i]: the run rz = (1, 1) z1 −→s1 z2 −→s2··· zi −→si zi+1 −−−→si+1 is such thatsj zj+1 −−−→··· zi −→si zi+1 −−−→si+1 is a non-safe run that does not visitSSync, and starts and ends in the same safe component. To reach a contradiction, we show that the latter run can be extended to a non-safe cy...

View on Pith

[22] [22]

q∈S (v) for some vertexv∈ V and ai = v′ for somev′ vertex withd(v,v′)≤ 2, or ai = ˆv′ for some vertexv′ with d(v,v′) = 1, orai = ˇv. Thus,ai corresponds to the values of vertices of distance at most2 from v, or the hat values of neighbors ofv, or the check Bader Abu Radi and Rüdiger Ehlers 35 value ofv

View on Pith

[23] [23]

q∈S (v) for some vertexv̸=v1 and ai =v1

View on Pith

[24] [24]

q∈S Sync and ai = extra, orai∈V is a vertex withd(v1,ai)≤ 1. Thus,ai corresponds to the values of vertices in the neighborhood ofv1, or the value ofextra. ▶ Remark 27. Consider a stateq∈ Q, and an atomic propositionai∈ AP. When ai is essential toq, then the assignment ofai is essential not only for determining safe transitions insideAGv1 , but also for de...

View on Pith

[25] [25]

All runs of(e(AGv1 ))s on⟨σ⟩ end in a state inQ. In addition, if a runr =s ⟨σ⟩ −−→p exists in e(AGv1 ), then it is unique, and is of the formr =s,s⟨σ⟩[1,1],s⟨σ⟩[1,2],...,s ⟨σ⟩[1,k−1],p. 38 Characterizing the Polynomial-Time Minimizable ω-Automata

View on Pith

[26] [26]

The triple⟨s,σ,p⟩ is a transition ofAGv1 iff there is a runr =s ⟨σ⟩ −−→p in e(AGv1 ). In addition, the runr is safe only when the transition⟨s,σ,p⟩ is safe. Proof. 1. Is immediate from the definition ofe(AGv1 ). Indeed, upon reading⟨σ⟩ from s, we move deterministically via safe transitions to the states⟨σ⟩[1,i] after reading thei’th bit of⟨σ⟩ for alli∈ [k...

View on Pith

[27] [27]

Consider a triplet =⟨s,σ,p⟩∈ Q× Σ×Q. By the definition ofe(AGv1 ), we know that there is a safe run of the forms ⟨σ⟩[1,k−1] −−−−−−→s⟨σ⟩[1,k−1] in e(AGv1 ). In addition, the above run can be extended to a runr from s on⟨σ⟩ to p only when the triplet =⟨s,σ,p⟩ is a transition ofAGv1 . The definition of the acceptance condition ofe(AGv1 ) implies that the run...

View on Pith

[28] [28]

The run of e(AGv1p )⟨s,i1⟩ on ⟨σ⟩ ends in a state in Qv1,p. In addition, if a run r = ⟨s,i 1⟩ ⟨σ⟩ −−→ ⟨q,i 2⟩ exists in e(AGv1p ), then it is unique, and is of the form r =⟨s,i 1⟩,⟨s⟨σ⟩[1,1],i 1⟩,⟨s⟨σ⟩[1,2],i 1⟩,..., ⟨s⟨σ⟩[1,k−1],i 1⟩,⟨q,i 2⟩

View on Pith

[29] [29]

The triple⟨⟨s,i 1⟩,σ,⟨q,i 2⟩⟩ is a transition ofAGv1p iff there is a runr =⟨s,i 1⟩ ⟨σ⟩ −−→⟨q,i 2⟩ in e(AGv1p ). In addition, the runr is safe only when the transition⟨⟨s,i 1⟩,σ,⟨q,i 2⟩⟩ is safe. Proof. The proof is similar to that of Lemma 30 and is immediate from the definitions. Specifically, when reading⟨σ⟩ from⟨s,i 1⟩, we move deterministically to the...

View on Pith