Disambiguabilità e Minimizzazione dei Registri di Modelli Min-Plus

Informazioni Fondamentali

• ID Articolo: 2512.09484
• Titolo: Unambiguisability and Register Minimisation of Min-Plus Models
• Autori: Shaull Almagor, Guy Arbel, Sarai Sheinvald (Technion – Israel Institute of Technology)
• Classificazione: cs.FL (Formal Languages and Automata Theory)
• Data di Pubblicazione: Dicembre 2025 (preprint arXiv)
• Link Articolo: https://arxiv.org/abs/2512.09484

Riassunto

Questo articolo studia il problema della disambiguabilità per automi finiti pesati (WFA) nel semianello min-plus (tropicale), nonché il problema della minimizzazione dei contatori per automi a registri di costo (CRA) tropicali, che hanno potenza espressiva equivalente ai WFA. Entrambi i problemi investigano se il "grado di non-determinismo" nel modello può essere ridotto. Gli autori dimostrano che il problema della disambiguabilità dei WFA è decidibile, risolvendo così un problema aperto di lunga data. Il metodo di prova consiste in una riduzione al problema della determinizzazione dei WFA (recentemente provato decidibile). Come risultato negativo, gli autori provano che il problema della minimizzazione dei contatori dei CRA è indecidibile, anche per un numero fisso di registri (specificamente sette registri).

Contesto di Ricerca e Motivazione

1. Problemi di Ricerca

L'articolo studia due problemi fondamentali:

• Problema di disambiguabilità: Dato un automa finito pesato A, esiste un automa non-ambiguo equivalente?
• Problema di minimizzazione dei registri: Dato un automa a registri di costo con k registri, esiste un automa a registri di costo equivalente con (k-1) registri?

2. Importanza del Problema

• Significato teorico: Gli automi finiti pesati sono importanti modelli di calcolo quantitativo che definiscono funzioni da parole a valori. I WFA sul semianello tropicale (Z∪{∞}, min, +) hanno ampie applicazioni nella modellazione di sistemi e possono essere utilizzati per ragionare sui modi ottimali di utilizzo delle risorse (come il consumo energetico).
• Valore pratico: L'esistenza di non-determinismo rende il ragionamento sui WFA più difficile. Ad esempio, il problema dell'equivalenza per WFA tropicali è indecidibile per automi non-deterministici, ma decidibile per automi deterministici.
• Posizione storica: I WFA tropicali hanno svolto un ruolo cruciale nella risoluzione della congettura dell'altezza delle stelle.

3. Limitazioni dei Metodi Esistenti

• Il problema della determinizzazione è stato provato decidibile solo recentemente (2025)
• Per automi tropicali con ambiguità polinomiale, il problema della disambiguabilità è stato provato decidibile, ma il caso generale rimane aperto
• Il problema della disambiguabilità sul campo dei numeri razionali è decidibile, ma la situazione sul semianello tropicale non era risolta
• Nella maggior parte dei modelli, i problemi di determinizzazione e disambiguabilità vengono solitamente risolti contemporaneamente, ma i WFA tropicali presentano un caso speciale

4. Motivazione della Ricerca

• Gli WFA non-ambigui hanno potenza espressiva strettamente maggiore rispetto ai WFA deterministici, ma conservano alcune buone proprietà di chiusura e algoritmiche
• Il non-determinismo può essere misurato in vari modi: l'ambiguità e la larghezza fornono prospettive diverse
• Il numero di registri corrisponde alla larghezza del WFA, fornendo un altro modo di misurare il non-determinismo

Contributi Principali

I principali contributi dell'articolo includono:

1. Risoluzione di un problema aperto di lunga data: Viene provato che il problema della disambiguabilità per WFA tropicali è decidibile, un problema che rimane irrisolto da lungo tempo.
2. Metodo di riduzione innovativo: Il problema della disambiguabilità viene risolto attraverso una riduzione al problema della determinizzazione. Questo è in qualche modo controintuitivo, poiché solitamente si risolve prima la disambiguabilità e poi la determinizzazione.
3. Nuova caratterizzazione dei gap: Viene introdotto il concetto di testimone di gap di tipo U (U-type gap witness), fornendo una caratterizzazione completa della disambiguabilità.
4. Risultato negativo: Viene provato che il problema della minimizzazione dei registri dei CRA è indecidibile, anche fissando il numero di registri a sette.
5. Risultati di equivalenza: Vengono raffinati i rapporti di equivalenza tra k-CRA e WFA di larghezza k.

Spiegazione Dettagliata dei Metodi

Definizione dei Compiti

Problema di Disambiguabilità (Problema 2):

• Input: Un WFA A
• Output: Determinare se esiste un WFA non-ambiguo equivalente
• Definizione: Un WFA A è non-ambiguo se e solo se ogni parola ha al massimo un'esecuzione accettante

Problema di Minimizzazione dei Registri:

• Input: Un CRA con k registri
• Output: Determinare se esiste un CRA equivalente con (k-1) registri

Architettura del Metodo Principale

1. Caratterizzazione dei Gap di Tipo U (Sezione 3)

Definizione 5 (Testimone di Gap di Tipo U B): Per B ∈ N, un testimone di gap di tipo U B consiste di coppie di parole x, y ∈ Σ* e stati p₁, q₁ ∈ Q, p₂, q₂ ∈ F con esecuzioni:

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

che soddisfano:

1. mwt(q₀ →^x Q) = wt(χx) (il prefisso di χ è l'esecuzione di peso minimo su x)
2. mwt(q₀ →^xy F) = wt(ρ) (ρ è l'esecuzione accettante di peso minimo su xy)
3. wt(ρx) - wt(χx) > B (dopo aver letto x, ρ è superiore di almeno B rispetto all'esecuzione minima)

Teorema 6: Un WFA A può essere disambiguato se e solo se esiste B ∈ N tale che i gap di A siano limitati da B.

2. Costruzione della Disambiguabilità (Sezione 3.2)

Dato un WFA A i cui gap sono limitati da B, si costruisce un WFA non-ambiguo equivalente U:

Spazio degli stati: S = Q × B-Win, dove B-Win = {-∞, -B, ..., B, ∞}^Q

Idea principale:

• Tracciare l'esecuzione minima canonica
• Utilizzare una finestra B per registrare gli offset di peso di ogni stato rispetto allo stato tracciato corrente
• Selezionare un'unica esecuzione canonica tra più esecuzioni minime attraverso un ordinamento di priorità (ordine lineare ⪯)

Definizione della relazione di transizione Λ: Per uno stato (q, f_q) e una lettera σ, considerare la transizione (q, σ, c, p):

1. Calcolare la funzione intermedia g(p) = min{f_q(r) + mwt(r →^σ p) - c | r ∈ Q}
2. Controllo di coerenza:
   • Se g(p) < 0, non aggiungere la transizione (esiste un'esecuzione di peso inferiore)
   • Se esiste r ≠ q e q ⪯ r tale che f_q(r) + mwt(r →^σ p) - c = g(p), non aggiungere la transizione (esiste un'esecuzione di priorità superiore)
3. Troncare g a -B, B per ottenere f_p

Stati accettanti: G = {(q, f_q) | q ∈ F ∧ ∀p ∈ F, (f_q(p) > 0 ∨ (f_q(p) = 0 ∧ p ⪯ q))}

3. Riduzione alla Determinizzazione (Sezione 4)

Idea principale: Costruire un WFA B tale che A può essere disambiguato se e solo se B può essere determinizzato.

Dettagli della costruzione:

• Stati: S = Q × Com, dove Com = {⊥, ↛, →}^Q (funzioni di impegno)
• Alfabeto: Γ = Σ × Updt, dove Updt = {⊥, ↛, →}^(Q×Q) (funzioni di aggiornamento)
• Semantica dell'impegno:
  • →: lo stato è raggiungibile e su un'esecuzione accettante
  • ↛: lo stato è raggiungibile ma non su un'esecuzione accettante
  • ⊥: lo stato non è raggiungibile

Condizioni di coerenza:

1. Coerenza Δ: la proiezione su A è una transizione valida
2. Coerenza dell'aggiornamento: α riflette correttamente le transizioni disponibili su σ
3. Coerenza dei bordi in uscita: f(r) = → se e solo se esiste r' tale che r → r' ∈ α
4. Coerenza dei bordi in entrata: g(r') = → se e solo se esiste r tale che r → r' ∈ α

Lemmi chiave:

• Lemma 15: Se esiste un testimone di gap di tipo U B in A, allora esiste un testimone di gap di tipo D B in B
• Lemma 16: Se esiste un testimone di gap di tipo D B in B, allora esiste un testimone di gap di tipo U B in A

Punti di Innovazione Tecnica

1. Innovazione nella caratterizzazione dei gap:
   • Introduzione del testimone di gap di tipo U, distinto dal testimone di gap di tipo D già noto
   • Il tipo U richiede che anche l'"esecuzione bassa" possa continuare fino a uno stato accettante, che è la differenza chiave rispetto al tipo D
2. Costruzione dell'esecuzione canonica:
   • Filtraggio progressivo delle esecuzioni minime da dietro in avanti attraverso un ordine lineare ⪯
   • Garantisce l'unicità mantenendo la proprietà di peso minimo
3. Design astuto della riduzione:
   • Utilizzo di meccanismi di impegno e aggiornamento per forzare i testimoni di tipo D di B a essere anche testimoni di tipo U di A
   • Controlli di coerenza garantiscono l'estendibilità delle esecuzioni basse
4. Equivalenza tra larghezza e registri:
   • Stabilimento preciso della conversione bidirezionale tra k-CRA e WFA di larghezza k
   • Nella direzione WFA→CRA, l'innovazione chiave è il riutilizzo dei registri piuttosto che l'allocazione di registri indipendenti per ogni stato

Configurazione Sperimentale

Questo articolo è un lavoro puramente teorico e non include valutazioni sperimentali. Tutti i risultati sono ottenuti attraverso prove matematiche rigorose.

Struttura della Prova

1. Decidibilità della disambiguabilità (Sezioni 3-4):
   • Sezione 3: Prova della necessità e sufficienza della caratterizzazione dei gap
   • Sezione 4: Riduzione al problema della determinizzazione
2. Indecidibilità della minimizzazione dei registri (Sezione 5):
   • Riduzione dal problema dell'arresto a 0 di macchine a due contatori
   • Utilizzo della costruzione del Teorema 22 (da 2)
   • Costruzione di un WFA di larghezza 7, prova che non può essere ridotto a larghezza 6

Strumenti Teorici

• Tecnica dei testimoni di gap: Derivata dalla ricerca sul problema della determinizzazione
• Costruzione per sottoinsiemi: Utilizzata per la conversione da CRA a WFA
• Rappresentazione matriciale: Utilizzata per la semantica dei CRA
• Tecnica di riduzione: Da problemi indecidibili (macchine a due contatori) al problema target

Risultati Sperimentali

Risultati Teorici Principali

1. Decidibilità della Disambiguabilità (Teorema 13 + Corollario 17)

Teorema 13: Il problema della disambiguabilità si riduce al problema della determinizzazione.

Corollario 17: Il problema della disambiguabilità per WFA è decidibile.

Punti chiave della prova:

• Direzione positiva: Se B può essere determinizzato, allora A può essere disambiguato
  • Utilizzo del Lemma 16: i testimoni di tipo D di B implicano testimoni di tipo U di A
  • Attraverso il meccanismo di impegno, la coerenza dei bordi in entrata garantisce che le esecuzioni basse si estendano a stati accettanti
• Direzione negativa: Se A può essere disambiguato, allora B può essere determinizzato
  • Utilizzo del Lemma 15: i testimoni di tipo U di A sono automaticamente testimoni di tipo D di B
  • La proiezione conserva il peso e la minimalità

2. Indecidibilità della Minimizzazione dei Registri (Teorema 20)

Teorema 20: Il seguente problema è indecidibile, anche per k=7: dato un WFA di larghezza k, determinare se esiste un WFA equivalente di larghezza k-1.

Corollario 21: Il seguente problema è indecidibile, anche per k=7: dato un k-CRA, determinare se esiste un (k-1)-CRA equivalente.

Strategia di prova:

1. Dalla macchina a due contatori M si costruisce un WFA di larghezza 6 A (Teorema 22)
2. Estensione di A per ottenere un WFA di larghezza 7 A', aggiungendo:
   • Stati q_a e q_i (i∈6)
   • Lettere $, i, a, ī_i
3. Se il limite su A è limitato, allora q_a è ridondante e si può ottenere un WFA equivalente di larghezza 6
4. Se A è illimitato, allora esiste ζ=x@ tale che q₀ →^ζ q₀ ha peso 1
5. Utilizzo della parola w = ζ^(6m) 1^(5m) 2^(4m) ... 5^m e del suffisso x = a ī₁ī₂...ī₅ per costruire una contraddizione:
   • 7 prefissi x₀,...,x₆ tali che A'(wx_i) = im
   • Principio della piccionaia: almeno due prefissi i<j raggiungono lo stesso stato t
   • Differenza di peso (j-i)m ≤ 12||B||, in contraddizione con m > 12||B||

Analisi della Complessità

Problema della disambiguabilità:

• Limite inferiore: PSPACE-hard (ereditato dal limite inferiore del problema della determinizzazione)
• Limite superiore: Sconosciuto (il limite superiore della complessità del problema della determinizzazione non è ancora stabilito)
• Complessità della riduzione: Espansione dello spazio degli stati singolarmente esponenziale

Problema della minimizzazione dei registri:

• Per k fisso ≥7: indecidibile
• Per k<7: problema aperto
• Per CRA su campi razionali: decidibile (6)

Intuizioni Tecniche Chiave

1. Essenza della limitazione dei gap:
   • La caratterizzazione dei gap di tipo U cattura il "grado di separazione" di due esecuzioni accettanti
   • I gap limitati garantiscono che sia possibile tracciare tutte le esecuzioni rilevanti con una finestra finita
2. Determinizzazione vs Disambiguabilità:
   • Solitamente si risolve prima la disambiguabilità, poi la determinizzazione
   • Sul semianello tropicale è il contrario: si risolve prima la determinizzazione, poi si riduce la disambiguabilità
   • Motivo: il meccanismo di impegno può "forzare" i testimoni di tipo D a diventare testimoni di tipo U
3. Incomprimibilità della larghezza:
   • I 7 componenti (q_a e q_1,...,q_6) attraverso parole e lettere di uccisione accuratamente progettate producono configurazioni di peso non-fusibili
   • Ogni componente raggiunge il minimo in momenti diversi, impossibile da simulare con 6 registri

Lavori Correlati

1. Ricerca sul Problema della Determinizzazione

• Storia: Risale agli anni '90 19, 20
• Campo razionale: Recentemente provato decidibile 5, 14
• Semianello tropicale: Provato decidibile nel 2025 1 (lavoro precedente degli autori)
• Caratterizzazione dei gap: Filiot et al. 11 hanno introdotto il concetto di gap di tipo D

2. Ricerca sull'Ambiguità

• Classificazione: k-ambiguità, ambiguità finita, ambiguità polinomiale 7
• Ambiguità polinomiale: Kirsten e Lombardy 16 provano che la disambiguabilità per automi tropicali è decidibile
• Campo razionale: Bell e Smertnig 5 provano la decidibilità
• Contributo di questo articolo: Risoluzione del caso generale (ambiguità arbitraria)

3. Automi a Registri di Costo

• Introduzione: Alur et al. 4 definiscono il modello CRA
• Potenza espressiva: Equivalente ai WFA 4
• Minimizzazione dei registri:
  • Campo razionale: decidibile 6
  • Semianello tropicale: provato indecidibile in questo articolo
• CRA deboli: Almagor et al. 3 studiano CRA copyless

4. Applicazioni del Semianello Tropicale

• Problema dell'altezza delle stelle: Lavori di Hashiguchi 12, 13, Kirsten 15
• Problema di limitazione: Leung e Podolskiy 18
• Limitatezza del limite superiore: Almagor et al. 2 provano l'indecidibilità (base della riduzione della minimizzazione dei registri in questo articolo)

Contributi Unici di Questo Articolo

1. Primo a risolvere il problema generale della disambiguabilità per WFA tropicali
2. Direzione innovativa: Riduzione al problema della determinizzazione piuttosto che costruzione diretta
3. Quadro completo: Risultati positivi (decidibilità della disambiguabilità) e negativi (indecidibilità della minimizzazione dei registri) simultaneamente
4. Caratterizzazione fine: Stabilimento della corrispondenza precisa tra k-CRA e WFA di larghezza k

Conclusioni e Discussione

Conclusioni Principali

1. Risultato di decidibilità: Il problema della disambiguabilità per WFA tropicali è decidibile, risolvendo un problema aperto di lunga data.
2. Risultato di indecidibilità: Il problema della minimizzazione dei registri dei CRA è indecidibile anche per un numero fisso di 7 registri.
3. Contributo metodologico: La risoluzione del problema della disambiguabilità attraverso riduzione al problema della determinizzazione rivela profonde connessioni tra i problemi.
4. Raffinamento dell'equivalenza: Equivalenza precisa tra k-CRA e WFA di larghezza k.

Limitazioni

1. Complessità sconosciuta:
   • La complessità precisa del problema della disambiguabilità non è determinata
   • Si conosce solo il limite inferiore PSPACE-hard
   • La riduzione ha espansione singolarmente esponenziale, se necessaria rimane sconosciuto
2. Gap nella minimizzazione dei registri:
   • Indecidibile per k=7
   • La decidibilità per k<7 rimane un problema aperto
   • Per k=1 (determinizzazione) è decidibile
3. Ambiguità rilassata:
   • La decidibilità generale della 2-disambiguabilità, ambiguità finita, disambiguabilità con ambiguità polinomiale rimane irrisolta
   • Mancano caratterizzazioni di gap corrispondenti
4. Frammenti speciali:
   • La decidibilità della minimizzazione dei registri per CRA copyless rimane sconosciuta
   • I casi sotto altre restrizioni strutturali non sono stati esplorati

Direzioni Future

Problemi aperti esplicitamente proposti dagli autori:

1. Ambiguità rilassata:
   • È possibile determinare se un dato WFA ha un equivalente WFA con 2-ambiguità/ambiguità finita/ambiguità polinomiale?
   • Il problema della 2-disambiguabilità sembra estremamente difficile, attualmente non esiste un criterio di gap corrispondente
2. Completamento del quadro della minimizzazione dei registri:
   • La minimizzazione dei registri è decidibile per k<7?
   • Sebbene di importanza minore, una caratterizzazione completa rimane di valore
3. Frammenti strutturali:
   • Minimizzazione dei registri per CRA copyless
   • Proprietà di altre classi di CRA ristrette
4. Definizione della complessità:
   • Determinazione della complessità precisa del problema della disambiguabilità
   • Una volta definita la complessità della determinizzazione, investigare se la riduzione può essere migliorata (tempo polinomiale o spazio logaritmico)

Valutazione Approfondita

Punti di Forza

1. Progresso teorico significativo:
   • Risoluzione del problema aperto di lunga data della disambiguabilità
   • Approccio metodologico innovativo: utilizzo inverso della determinizzazione per risolvere la disambiguabilità
   • Tecniche di prova profonde ed eleganti
2. Quadro teorico completo:
   • Coesistenza di risultati positivi (decidibilità) e negativi (indecidibilità)
   • Stabilimento di connessioni tra diversi modelli (WFA e CRA) e diverse metriche (ambiguità e larghezza)
3. Innovazione tecnica significativa:
   • Caratterizzazione dei gap di tipo U: cattura precisa dell'essenza della non-ambiguità
   • Costruzione dell'esecuzione canonica: realizzazione dell'unicità attraverso ordinamento di priorità
   • Meccanismo di impegno: trasformazione astuta dei testimoni di tipo D in testimoni di tipo U
   • Riutilizzo dei registri: evitamento dell'espansione esponenziale nella conversione WFA→CRA
4. Prove rigorose e complete:
   • Tutti i teoremi hanno prove dettagliate
   • Logica chiara tra i lemmi
   • Giustificazione sufficiente dei punti tecnici chiave (come Lemmi 8, 9)
5. Alta qualità della scrittura:
   • Struttura chiara, progressione da motivazione a risultati
   • Buona combinazione di spiegazioni intuitive e definizioni formali
   • Diagrammi (come Figure 1-5) facilitano la comprensione

Punti Deboli

1. Mancanza di limiti di complessità:
   • Limite superiore sconosciuto per il problema della disambiguabilità
   • Analisi mancante sulla necessità dell'espansione della riduzione
   • Valutazione mancante della calcolabilità pratica
2. Gap nella minimizzazione dei registri:
   • Il limite k=7 è stretto?
   • I casi k∈{2,3,4,5,6} rimangono completamente aperti
   • Il punto di transizione da k=1 (decidibile) a k=7 (indecidibile) non è determinato
3. Problemi di ambiguità rilassata non affrontati:
   • Problemi come la 2-disambiguabilità sono solo menzionati nella discussione
   • Nessun indizio tecnico o risultato parziale fornito
4. Mancanza di considerazioni pratiche:
   • Lavoro puramente teorico, nessuna implementazione di algoritmi
   • Nessuna analisi di complessità o discussione di fattibilità
   • Guida limitata per applicazioni pratiche
5. Generalizzabilità delle tecniche di prova:
   • Se i metodi sono applicabili ad altri semianelli non è discusso
   • La relazione con i risultati già noti su campi razionali non è analizzata in profondità

Valutazione dell'Impatto

1. Significato teorico considerevole:
   • Risoluzione di un problema aperto di lunga data, previsto di diventare una pietra miliare nel campo
   • Fornitura di nuovi strumenti per ricerche successive (gap di tipo U, meccanismo di impegno)
   • Rivelazione di connessioni profonde tra determinizzazione e disambiguabilità
2. Contributo metodologico:
   • Le tecniche di riduzione potrebbero ispirare la soluzione di altri problemi
   • Il metodo di caratterizzazione dei gap potrebbe essere generalizzato ad altri modelli
3. Ispirazione per problemi aperti:
   • Chiara indicazione di importanti direzioni di ricerca successive
   • Fornitura di benchmark per la minimizzazione dei registri con k<7
4. Limitazione dell'impatto dovuta a limitazioni:
   • Mancanza di limiti di complessità limita le applicazioni pratiche
   • Algoritmi e implementazione richiedono ulteriori lavori

Scenari di Applicabilità

1. Ricerca teorica:
   • Teoria dei linguaggi formali e teoria degli automi
   • Teoria della decidibilità e della complessità
   • Modelli di calcolo su semianelli
2. Verifica di sistemi:
   • Sistemi che richiedono ragionamento sul consumo di risorse (energia, tempo)
   • Semplificazione di automi nella verifica quantitativa
3. Progettazione di algoritmi:
   • Ottimizzazione e trasformazione di automi pesati
   • Misurazione e controllo del non-determinismo
4. Valore didattico:
   • Dimostrazione della potenza delle tecniche di riduzione
   • Illustrazione della sottigliezza dei confini della decidibilità

Riepilogo dei Punti Tecnici Salienti

1. Caratterizzazione precisa dei gap di tipo U: Cattura perfetta dell'essenza combinatoria della non-ambiguità
2. Costruzione dell'esecuzione canonica: Risoluzione del problema dell'unicità attraverso un semplice meccanismo di priorità
3. Design del meccanismo di impegno: Codifica esplicita del DAG di esecuzione nell'alfabeto, forzamento della coerenza
4. Strategia di riutilizzo dei registri: Realizzazione della corrispondenza precisa di larghezza mantenendo l'equivalenza
5. Eleganza della prova di indecidibilità: Arrangiamento astuto di 7 componenti per dimostrare l'incomprimibilità

Riferimenti Bibliografici (Riferimenti Chiave)

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.

Valutazione Complessiva: Questo articolo rappresenta un importante contributo teorico nel campo della teoria dei linguaggi formali e della teoria degli automi, risolvendo il problema aperto di lunga data della disambiguabilità e rivelando l'indecidibilità della minimizzazione dei registri. Le tecniche di prova sono profonde e innovative, in particolare l'approccio controintuitivo di utilizzare la riduzione al problema della determinizzazione. Sebbene manchino limiti di complessità e algoritmi pratici, il valore teorico e il contributo metodologico lo rendono un progresso importante nel campo. Per i ricercatori in informatica teorica, questo è un articolo imprescindibile.