Eindeutigkeit und Registerminimierung von Min-Plus-Modellen

Grundlegende Informationen

• Papier-ID: 2512.09484
• Titel: Unambiguisability and Register Minimisation of Min-Plus Models
• Autoren: Shaull Almagor, Guy Arbel, Sarai Sheinvald (Technion – Israel Institute of Technology)
• Klassifikation: cs.FL (Formale Sprachen und Automatentheorie)
• Veröffentlichungsdatum: Dezember 2025 (arXiv-Preprint)
• Papier-Link: https://arxiv.org/abs/2512.09484

Zusammenfassung

Dieses Papier untersucht das Eindeutigkeitsproblem für Min-Plus-(tropische) gewichtete endliche Automaten (WFAs) sowie das Registerminimierungsproblem für tropische Kostenregisterautomaten (CRAs), die äquivalent zu WFAs sind. Beide Probleme stellen die Frage, ob der „Grad der Nichtdeterminismus" in einem Modell reduziert werden kann. Die Autoren zeigen, dass das WFA-Eindeutigkeitsproblem entscheidbar ist und lösen damit ein lange offenes Problem. Der Beweis erfolgt durch Reduktion auf das WFA-Determinisierungsproblem (das kürzlich als entscheidbar nachgewiesen wurde). Als negatives Ergebnis zeigen die Autoren, dass das CRA-Registerminimierungsproblem unentscheidbar ist, selbst für eine feste Anzahl von Registern (konkret sieben Register).

Forschungshintergrund und Motivation

1. Forschungsfragen

Dieses Papier untersucht zwei zentrale Probleme:

• Eindeutigkeitsproblem: Gegeben ein gewichteter endlicher Automat A, existiert ein äquivalenter eindeutiger Automat?
• Registerminimierungsproblem: Gegeben ein k-Register-Kostenregisterautomat, existiert ein äquivalenter (k-1)-Register-Automat?

2. Bedeutung der Probleme

• Theoretische Bedeutung: Gewichtete endliche Automaten sind wichtige Modelle für quantitative Berechnung und definieren Funktionen von Wörtern zu Werten. WFAs über dem tropischen Halbring (Z∪{∞}, min, +) haben breite Anwendungen in der Systemmodellierung und können zur Analyse optimaler Ressourcennutzung (z.B. Energieverbrauch) verwendet werden.
• Praktischer Wert: Die Existenz von Nichtdeterminismus macht Schlussfolgerungen über WFAs schwieriger. Beispielsweise ist das Äquivalenzproblem für tropische WFAs für nichtdeterministische Automaten unentscheidbar, aber für deterministische Automaten entscheidbar.
• Historische Bedeutung: Tropische WFAs spielten eine Schlüsselrolle bei der Lösung der Star-Height-Vermutung.

3. Einschränkungen bestehender Methoden

• Das Determinisierungsproblem wurde erst kürzlich (2025) als entscheidbar nachgewiesen
• Für tropische Automaten mit polynomialer Mehrdeutigkeit wurde das Eindeutigkeitsproblem als entscheidbar nachgewiesen, der allgemeine Fall blieb jedoch offen
• Das Eindeutigkeitsproblem über rationalen Zahlen ist entscheidbar, aber die Situation über dem tropischen Halbring war ungeklärt
• In den meisten Modellen werden Determinisierungs- und Eindeutigkeitsprobleme typischerweise gleichzeitig gelöst, aber tropische WFAs sind ein Sonderfall

4. Forschungsmotivation

• Eindeutige WFAs sind streng ausdrucksstärker als deterministische WFAs, bewahren aber einige gute Abschluss- und Algorithmuseigenschaften
• Nichtdeterminismus kann auf verschiedene Weise gemessen werden: Mehrdeutigkeit (ambiguity) und Breite (width) bieten unterschiedliche Perspektiven
• Die Registeranzahl entspricht der Breite eines WFA und bietet eine alternative Methode zur Messung von Nichtdeterminismus

Kernbeiträge

Die Hauptbeiträge dieses Papiers sind:

1. Lösung eines lange offenen Problems: Nachweis, dass das Eindeutigkeitsproblem für tropische WFAs entscheidbar ist, ein lange ungelöstes Problem.
2. Innovative Reduktionsmethode: Lösung des Eindeutigkeitsproblems durch Reduktion auf das Determinisierungsproblem. Dies ist in gewisser Weise kontraintuitiv, da normalerweise zuerst das Eindeutigkeitsproblem gelöst wird, dann das Determinisierungsproblem.
3. Neue Lückenkennzeichnung: Einführung des Konzepts von U-Typ-Lückenzeugen, die eine vollständige Kennzeichnung der Eindeutigkeit bieten.
4. Negative Ergebnisse: Nachweis, dass das CRA-Registerminimierungsproblem unentscheidbar ist, selbst wenn die Registeranzahl auf 7 festgelegt ist.
5. Äquivalenzergebnisse: Verfeinerung der Äquivalenzbeziehung zwischen k-CRA und WFAs der Breite k.

Methodische Details

Aufgabendefinition

Eindeutigkeitsproblem (Problem 2):

• Eingabe: Ein WFA A
• Ausgabe: Entscheidung, ob ein äquivalenter eindeutiger WFA existiert
• Definition: Ein WFA A ist eindeutig, wenn und nur wenn jedes Wort höchstens einen akzeptierenden Lauf hat

Registerminimierungsproblem:

• Eingabe: Ein k-Register-CRA
• Ausgabe: Entscheidung, ob ein äquivalenter (k-1)-Register-CRA existiert

Architektur der Kernmethode

1. U-Typ-Lückenkennzeichnung (Abschnitt 3)

Definition 5 (U-Typ B-Lückenzeuge): Für B ∈ ℕ besteht ein U-Typ B-Lückenzeuge aus Wortpaaren x, y ∈ Σ* und Zuständen p₁, q₁ ∈ Q, p₂, q₂ ∈ F mit Läufen:

• ρ: q₀ →^x p₁ →^y p₂
• χ: q₀ →^x q₁ →^y q₂

die erfüllen:

1. mwt(q₀ →^x Q) = wt(χx) (χ's Präfix ist der minimale Gewichtslauf auf x)
2. mwt(q₀ →^xy F) = wt(ρ) (ρ ist der minimale akzeptierende Lauf auf xy)
3. wt(ρx) - wt(χx) > B (nach dem Lesen von x ist ρ mindestens B höher als der minimale Lauf)

Theorem 6: Ein WFA A kann eindeutig gemacht werden, wenn und nur wenn ein B ∈ ℕ existiert, so dass die Lücken von A durch B begrenzt sind.

2. Konstruktion der Eindeutigkeit (Abschnitt 3.2)

Gegeben ein WFA A mit durch B begrenzten Lücken, konstruiere einen äquivalenten eindeutigen WFA U:

Zustandsraum: S = Q × B-Win, wobei B-Win = {-∞, -B, ..., B, ∞}^Q

Schlüsselidee:

• Verfolgung des kanonischen minimalen Laufs
• Verwendung eines B-Fensters zur Aufzeichnung von Gewichtsabweichungen jedes Zustands vom aktuell verfolgten Zustand
• Auswahl eines eindeutigen kanonischen Laufs aus mehreren minimalen Läufen durch Prioritätsordnung (lineare Ordnung ⪯)

Definition der Übergangsfunktion Λ: Für einen Zustand (q, f_q) und einen Buchstaben σ, betrachte den Übergang (q, σ, c, p):

1. Berechne die Zwischenfunktion g(p) = min{f_q(r) + mwt(r →^σ p) - c | r ∈ Q}
2. Konsistenzprüfung:
   • Wenn g(p) < 0, füge keinen Übergang hinzu (es existiert ein Lauf mit niedrigerem Gewicht)
   • Wenn ein r ≠ q existiert mit q ⪯ r, so dass f_q(r) + mwt(r →^σ p) - c = g(p), füge keinen Übergang hinzu (es existiert ein Lauf mit höherer Priorität)
3. Schneide g auf -B, B ab, um f_p zu erhalten

Akzeptierende Zustände: G = {(q, f_q) | q ∈ F ∧ ∀p ∈ F, (f_q(p) > 0 ∨ (f_q(p) = 0 ∧ p ⪯ q))}

3. Reduktion auf Determinisierung (Abschnitt 4)

Kernidee: Konstruiere einen WFA B, so dass A eindeutig gemacht werden kann, wenn und nur wenn B determinisierbar ist.

Konstruktionsdetails:

• Zustände: S = Q × Com, wobei Com = {⊥, ↛, →}^Q (Verpflichtungsfunktionen)
• Alphabet: Γ = Σ × Updt, wobei Updt = {⊥, ↛, →}^(Q×Q) (Aktualisierungsfunktionen)
• Verpflichtungssemantik:
  • →: Zustand ist erreichbar und auf einem akzeptierenden Lauf
  • ↛: Zustand ist erreichbar, aber nicht auf einem akzeptierenden Lauf
  • ⊥: Zustand ist nicht erreichbar

Konsistenzbedingungen:

1. Δ-Konsistenz: Projektion auf A ist ein gültiger Übergang
2. Aktualisierungskonsistenz: α reflektiert korrekt verfügbare Übergänge auf σ
3. Ausgangskantkonsistenz: f(r) = → wenn und nur wenn ein r' existiert mit r → r' ∈ α
4. Eingangskantkonsistenz: g(r') = → wenn und nur wenn ein r existiert mit r → r' ∈ α

Schlüssellemmata:

• Lemma 15: Wenn ein U-Typ B-Lückenzeuge in A existiert, dann existiert ein D-Typ B-Lückenzeuge in B
• Lemma 16: Wenn ein D-Typ B-Lückenzeuge in B existiert, dann existiert ein U-Typ B-Lückenzeuge in A

Technische Innovationen

1. Innovation in der Lückenkennzeichnung:
   • Einführung von U-Typ-Lückenzeugen, unterschiedlich von bekannten D-Typ-Lückenzeugen
   • U-Typ erfordert, dass auch der „niedrige Lauf" zu einem akzeptierenden Zustand fortgesetzt werden kann, dies ist der Schlüsselunterschied zu D-Typ
2. Konstruktion kanonischer Läufe:
   • Schrittweise Filterung minimaler Läufe durch lineare Ordnung ⪯ von hinten nach vorne
   • Gewährleistung der Eindeutigkeit bei Beibehaltung der minimalen Gewichtseigenschaft
3. Raffinierte Reduktionsgestaltung:
   • Verwendung von Verpflichtungs- und Aktualisierungsmechanismen zur Erzwingung, dass D-Typ-Zeugen von B auch U-Typ-Zeugen von A sind
   • Konsistenzprüfungen stellen sicher, dass niedrige Läufe erweiterbar sind
4. Äquivalenz von Breite und Registern:
   • Genaue Etablierung bidirektionaler Konvertierungen zwischen k-CRA und WFAs der Breite k
   • In der WFA→CRA-Richtung ist die Schlüsselinnovation die Wiederverwendung von Registern statt Zuweisung unabhängiger Register für jeden Zustand

Experimentelle Einrichtung

Dieses Papier ist eine rein theoretische Arbeit ohne experimentelle Bewertung. Alle Ergebnisse werden durch strenge mathematische Beweise erhalten.

Beweisstruktur

1. Entscheidbarkeit der Eindeutigkeit (Abschnitte 3-4):
   • Abschnitt 3: Nachweis der Notwendigkeit und Hinlänglichkeit der Lückenkennzeichnung
   • Abschnitt 4: Reduktion auf das Determinisierungsproblem
2. Unentscheidbarkeit der Registerminimierung (Abschnitt 5):
   • Reduktion vom Halteproblem mit zwei Zählern
   • Verwendung der Konstruktion aus Theorem 22 (aus 2)
   • Konstruktion eines WFA der Breite 7, Nachweis der Unmöglichkeit der Reduktion auf Breite 6

Theoretische Werkzeuge

• Lückenzeugtechnik: Stammt aus der Forschung zum Determinisierungsproblem
• Subset-Konstruktion: Verwendet für CRA-zu-WFA-Konvertierung
• Matrixdarstellung: Verwendet für CRA-Semantikdefinition
• Reduktionstechnik: Vom unentscheidbaren Problem (Zwei-Zähler-Maschine) zum Zielproblem

Experimentelle Ergebnisse

Haupttheoretische Ergebnisse

1. Entscheidbarkeit der Eindeutigkeit (Theorem 13 + Korollar 17)

Theorem 13: Das Eindeutigkeitsproblem ist auf das Determinisierungsproblem reduzierbar.

Korollar 17: Das WFA-Eindeutigkeitsproblem ist entscheidbar.

Beweisskizze:

• Vorwärtsrichtung: Wenn B determinisierbar ist, dann ist A eindeutig machbar
  • Verwendung von Lemma 16: D-Typ-Zeugen von B implizieren U-Typ-Zeugen von A
  • Durch Verpflichtungsmechanismus wird sichergestellt, dass niedrige Läufe zu akzeptierenden Zuständen erweiterbar sind
• Rückwärtsrichtung: Wenn A eindeutig machbar ist, dann ist B determinisierbar
  • Verwendung von Lemma 15: U-Typ-Zeugen von A sind automatisch D-Typ-Zeugen von B
  • Projektion bewahrt Gewicht und Minimalität

2. Unentscheidbarkeit der Registerminimierung (Theorem 20)

Theorem 20: Das folgende Problem ist unentscheidbar, selbst für k=7: Gegeben ein WFA der Breite k, entscheide, ob ein äquivalenter WFA der Breite k-1 existiert.

Korollar 21: Das folgende Problem ist unentscheidbar, selbst für k=7: Gegeben ein k-CRA, entscheide, ob ein äquivalenter (k-1)-CRA existiert.

Bewesstrategie:

1. Konstruktion eines WFA der Breite 6 aus einer Zwei-Zähler-Maschine M (Theorem 22)
2. Erweiterung von A zu einem WFA der Breite 7, A', durch Hinzufügung von:
   • Zuständen q_a und q_i (i∈6)
   • Buchstaben $, i, a, ī_i
3. Wenn die obere Schranke von A begrenzt ist, ist q_a überflüssig, was einen äquivalenten WFA der Breite 6 ergibt
4. Wenn A unbegrenzt ist, existiert ζ=x@ mit q₀ →^ζ q₀ Gewicht 1
5. Verwendung des Wortes w = ζ^(6m) 1^(5m) 2^(4m) ... 5^m und Suffix x = a ī₁ī₂...ī₅ zur Konstruktion eines Widerspruchs:
   • 7 Präfixe x₀,...,x₆ so dass A'(wx_i) = im
   • Schubfachprinzip: Mindestens zwei Präfixe i<j erreichen denselben Zustand t
   • Gewichtsdifferenz (j-i)m ≤ 12||B||, im Widerspruch zu m > 12||B||

Komplexitätsanalyse

Eindeutigkeitsproblem:

• Untere Schranke: PSPACE-hart (geerbt von der unteren Schranke des Determinisierungsproblems)
• Obere Schranke: Unbekannt (die Komplexitätsschranke des Determinisierungsproblems ist noch nicht etabliert)
• Reduktionskomplexität: Einfache exponentielle Zustandsraumvergrößerung

Registerminimierungsproblem:

• Für festes k≥7: Unentscheidbar
• Für k<7: Offenes Problem
• Für CRA über rationalen Zahlen: Entscheidbar (6)

Schlüsseltechnische Einsichten

1. Wesen der Lückenbegrenzung:
   • U-Typ-Lückenkennzeichnung charakterisiert den „Trennungsgrad" zweier akzeptierender Läufe
   • Begrenzte Lücken garantieren, dass alle relevanten Läufe mit einem endlichen Fenster verfolgt werden können
2. Determinisierung vs. Eindeutigkeit:
   • Normalerweise wird zuerst das Eindeutigkeitsproblem gelöst, dann das Determinisierungsproblem
   • Über dem tropischen Halbring umgekehrt: Zuerst Determinisierung, dann Reduktion auf Eindeutigkeit
   • Grund: Der Verpflichtungsmechanismus kann „D-Typ-Zeugen in U-Typ-Zeugen umwandeln"
3. Unkomprimierbarkeit der Breite:
   • 7 Komponenten (q_a und q_1,...,q_6) erzeugen durch sorgfältig gestaltete Wörter und Tötungsbuchstaben nicht zusammenführbare Gewichtskonfigurationen
   • Jede Komponente erreicht zu unterschiedlichen Zeiten das Minimum, kann nicht mit 6 Registern simuliert werden

Verwandte Arbeiten

1. Determinisierungsforschung

• Geschichte: Geht auf die 1990er Jahre zurück 19, 20
• Rationale Zahlen: Kürzlich als entscheidbar nachgewiesen 5, 14
• Tropischer Halbring: 2025 als entscheidbar nachgewiesen 1 (Vorarbeiten der Autoren)
• Lückenkennzeichnung: Filiot et al. 11 führten D-Typ-Lückenkonzept ein

2. Mehrdeutigkeitsforschung

• Klassifikation: k-Mehrdeutigkeit, endliche Mehrdeutigkeit, polynomiale Mehrdeutigkeit 7
• Polynomiale Mehrdeutigkeit: Kirsten und Lombardy 16 zeigen Entscheidbarkeit der Eindeutigkeit für tropische Automaten
• Rationale Zahlen: Bell und Smertnig 5 zeigen Entscheidbarkeit
• Beitrag dieses Papiers: Lösung des allgemeinen Falls (beliebige Mehrdeutigkeitsgrad)

3. Kostenregisterautomaten

• Einführung: Alur et al. 4 definieren CRA-Modell
• Ausdrucksstärke: Äquivalent zu WFA 4
• Registerminimierung:
  • Rationale Zahlen: Entscheidbar 6
  • Tropischer Halbring: Dieses Papier zeigt Unentscheidbarkeit
• Schwache CRA: Almagor et al. 3 untersuchen copyless CRA

4. Anwendungen des tropischen Halbringes

• Star-Height-Problem: Arbeiten von Hashiguchi 12, 13, Kirsten 15
• Beschränkungsproblem: Leung und Podolskiy 18
• Obere Schranken-Beschränktheit: Almagor et al. 2 zeigen Unentscheidbarkeit (Grundlage für die Registerminimierungsreduktion dieses Papiers)

Eindeutige Beiträge dieses Papiers

1. Erstmals Lösung des allgemeinen Eindeutigkeitsproblems für tropische WFAs
2. Innovative Richtung: Reduktion auf Determinisierung statt direkter Konstruktion
3. Vollständiges Bild: Gleichzeitig positive Ergebnisse (Entscheidbarkeit der Eindeutigkeit) und negative Ergebnisse (Unentscheidbarkeit der Registerminimierung)
4. Feine Kennzeichnung: Etablierung der genauen Entsprechung zwischen k-CRA und WFAs der Breite k

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

1. Entscheidbarkeitsergebnis: Das Eindeutigkeitsproblem für tropische WFAs ist entscheidbar, löst ein lange offenes Problem.
2. Unentscheidbarkeitsergebnis: Das CRA-Registerminimierungsproblem ist unentscheidbar, selbst für eine feste Anzahl von 7 Registern.
3. Methodologischer Beitrag: Lösung des Eindeutigkeitsproblems durch Reduktion auf das Determinisierungsproblem zeigt tiefe Verbindungen zwischen Problemen.
4. Verfeinerung der Äquivalenz: k-CRA und WFAs der Breite k sind genau äquivalent.

Einschränkungen

1. Unbekannte Komplexität:
   • Genaue Komplexität des Eindeutigkeitsproblems nicht bestimmt
   • Nur PSPACE-hart Untergrenze bekannt
   • Reduktion hat einfache exponentielle Vergrößerung, ob notwendig unklar
2. Lücke bei Registerminimierung:
   • Für k=7 unentscheidbar
   • Entscheidbarkeit für k<7 bleibt offenes Problem
   • Für k=1 (Determinisierung) ist es entscheidbar
3. Gelockerte Mehrdeutigkeit:
   • Allgemeine Entscheidbarkeit von 2-Eindeutigkeit, endlicher Mehrdeutigkeit, polynomialer Mehrdeutigkeit ungeklärt
   • Fehlende entsprechende Lückenkennzeichnung
4. Spezielle Fragmente:
   • Registerminimierung von copyless CRA ungeklärt
   • Andere strukturelle Einschränkungen nicht erforscht

Zukünftige Richtungen

Vom Autor explizit aufgeworfene offene Probleme:

1. Gelockerte Mehrdeutigkeit:
   • Kann man entscheiden, ob ein gegebener WFA einen äquivalenten 2-eindeutigen/endlich-eindeutigen/polynomisch-mehrdeutigen WFA hat?
   • Das 2-Eindeutigkeitsproblem scheint extrem schwierig, derzeit existiert kein entsprechendes Lückenkriterium
2. Vervollständigung des Registerminimierungsbildes:
   • Ist Registerminimierung für k<7 entscheidbar?
   • Obwohl weniger wichtig, ist eine vollständige Kennzeichnung noch wertvoll
3. Strukturelle Fragmente:
   • Registerminimierung von copyless CRA
   • Eigenschaften anderer eingeschränkter CRA-Klassen
4. Komplexitätsfestlegung:
   • Bestimmung der genauen Komplexität des Eindeutigkeitsproblems
   • Sobald die Komplexität der Determinisierung festgelegt ist, Untersuchung, ob die Reduktion verbessert werden kann (Polynomialzeit oder logarithmischer Raum)

Tiefgreifende Bewertung

Stärken

1. Großer theoretischer Durchbruch:
   • Lösung des lange offenen Eindeutigkeitsproblems
   • Neuartige Methode: Umgekehrte Nutzung der Determinisierung zur Lösung der Eindeutigkeit
   • Tiefe und elegante Beweistechniken
2. Vollständiges theoretisches Bild:
   • Positive Ergebnisse (Entscheidbarkeit) und negative Ergebnisse (Unentscheidbarkeit) koexistieren
   • Verbindung zwischen verschiedenen Modellen (WFA und CRA) und verschiedenen Maßstäben (Mehrdeutigkeit und Breite)
3. Bedeutende technische Innovationen:
   • U-Typ-Lückenkennzeichnung: Erfasst präzise das Wesen der Eindeutigkeit
   • Kanonische Laufkonstruktion: Realisiert Eindeutigkeit durch Prioritätsordnung
   • Verpflichtungsmechanismus: Wandelt D-Typ-Zeugen geschickt in U-Typ-Zeugen um
   • Registerwiederverwendung: Vermeidet exponentielle Vergrößerung in WFA→CRA-Konvertierung
4. Strenge und vollständige Beweise:
   • Alle Theoreme haben detaillierte Beweise
   • Logische Klarheit zwischen Lemmata
   • Ausreichende Argumentation für Schlüsseltechniken (z.B. Lemmata 8, 9)
5. Hohe Schreibqualität:
   • Klare Struktur, schrittweise Progression von Motivation zu Ergebnissen
   • Gute Kombination von intuitiver Erklärung und formaler Definition
   • Diagramme (z.B. Abbildungen 1-5) unterstützen das Verständnis

Schwächen

1. Fehlende Komplexitätsgrenzen:
   • Obere Schranke des Eindeutigkeitsproblems unbekannt
   • Ob die Reduktionsvergrößerung notwendig ist, nicht analysiert
   • Praktische Berechenbarkeit nicht bewertet
2. Lücke bei Registerminimierung:
   • Ist die Grenze k=7 scharf?
   • Fälle k∈{2,3,4,5,6} völlig offen
   • Übergangspunkt von k=1 (entscheidbar) zu k=7 (unentscheidbar) nicht bestimmt
3. Gelockerte Mehrdeutigkeitsprobleme nicht behandelt:
   • 2-Eindeutigkeit etc. nur in der Diskussion erwähnt
   • Keine technischen Hinweise oder Teilergebnisse bereitgestellt
4. Fehlende praktische Überlegungen:
   • Rein theoretische Arbeit, keine Algorithmusimplementierung
   • Keine Komplexitätsanalyse oder Machbarkeitsdiskussion
   • Begrenzte Anleitung für praktische Anwendungen
5. Verallgemeinerbarkeit der Beweistechniken:
   • Ob Methoden auf andere Halbringe anwendbar sind, nicht diskutiert
   • Beziehung zu bekannten Ergebnissen über rationalen Zahlen nicht tiefgehend analysiert

Bewertung der Auswirkungen

1. Große theoretische Bedeutung:
   • Lösung eines lange offenen Problems, erwartet als Meilenstein des Feldes
   • Bereitstellung neuer Werkzeuge für nachfolgende Forschung (U-Typ-Lücken, Verpflichtungsmechanismus)
   • Offenbarung tieferer Verbindungen zwischen Determinisierung und Eindeutigkeit
2. Methodologischer Beitrag:
   • Reduktionstechniken könnten andere Probleme inspirieren
   • Lückenkennzeichnungsmethode könnte auf andere Modelle verallgemeinert werden
3. Inspiration für offene Probleme:
   • Klare Angabe wichtiger Folgefragen
   • Bereitstellung von Benchmarks für Registerminimierung mit k<7
4. Einschränkung der Auswirkungen durch Schwächen:
   • Fehlende Komplexitätsgrenzen begrenzen praktische Anwendungen
   • Algorithmisierung und Implementierung erfordern weitere Arbeit

Anwendungsszenarien

1. Theoretische Forschung:
   • Formale Sprachen und Automatentheorie
   • Entscheidbarkeits- und Komplexitätstheorie
   • Berechnungsmodelle über Halbringe
2. Systemverifikation:
   • Systeme, die Ressourcenverbrauch (Energie, Zeit) analysieren müssen
   • Automatenvereinfachung in quantitativer Verifikation
3. Algorithmenentwurf:
   • Optimierung und Konvertierung gewichteter Automaten
   • Messung und Kontrolle von Nichtdeterminismus
4. Lehrwert:
   • Demonstration der Kraft von Reduktionstechniken
   • Illustration der Subtilität von Entscheidbarkeitsgrenzen

Zusammenfassung der technischen Highlights

1. Präzise U-Typ-Lückenkennzeichnung: Erfasst perfekt die kombinatorische Natur der Eindeutigkeit
2. Kanonische Laufkonstruktion: Löst das Eindeutigkeitsproblem durch einfachen Prioritätsmechanismus
3. Verpflichtungsmechanismus-Design: Kodiert Lauf-DAG explizit in das Alphabet, erzwingt Konsistenz
4. Registerwiederverwendungsstrategie: Realisiert genaue Breitenentsprechung bei Beibehaltung der Äquivalenz
5. Eleganz des Unentscheidbarkeitsnachweises: Sorgfältige Anordnung von 7 Komponenten zeigt Unkomprimierbarkeit

Referenzen (Schlüsselliteratur)

1 Almagor, Arbel, Sheinvald (2025). Determinization of min-plus weighted automata is decidable. SODA 2025.

2 Almagor, Boker, Kupferman (2020). What's decidable about weighted automata? Information and Computation.

4 Alur et al. (2013). Regular functions and cost register automata. LICS 2013.

5 Bell, Smertnig (2023). Computing the linear hull: Deciding determinizable and unambiguous for weighted automata over fields. LICS 2023.

11 Filiot et al. (2017). On delay and regret determinization of max-plus automata. LICS 2017.

16 Kirsten, Lombardy (2009). Deciding unambiguity and sequentiality of polynomially ambiguous min-plus automata. STACS 2009.

Gesamtbewertung: Dieses Papier ist ein wichtiger theoretischer Beitrag zur Formalen Sprachen- und Automatentheorie, löst das lange offene Eindeutigkeitsproblem und offenbart die Unentscheidbarkeit der Registerminimierung. Die Beweistechniken sind tiefgreifend und innovativ, insbesondere die umgekehrte Nutzung der Determinisierung zur Lösung der Eindeutigkeit. Obwohl Komplexitätsgrenzen und praktische Algorithmen fehlen, machen sein theoretischer Wert und methodologischer Beitrag es zu einem wichtigen Fortschritt in diesem Bereich. Für Forscher der theoretischen Informatik ist dies ein unverzichtbares Papier.