Positional $ω$-regular languages

Questo lavoro fornisce una caratterizzazione completa delle lingue $\omega$-regolari posizionali attraverso gli automi di parità, dimostrando la decidibilità in tempo polinomiale, l'esistenza di lift da giochi finiti a infiniti e da un giocatore a due, e la chiusura rispetto all'unione per obiettivi posizionali indipendenti dal prefisso, risolvendo così una congettura di Kopczyński.

L'essenziale

Immagina di essere il direttore di un'orchestra infinita. Hai due musicisti, chiamiamoli Eva e Adamo, che devono suonare insieme per sempre, prendendo decisioni a turno su quale nota suonare. L'obiettivo è creare una melodia infinita che soddisfi una regola specifica (ad esempio: "la nota 'Do' deve apparire infinite volte").

Il problema è: come può Eva assicurarsi di vincere, indipendentemente da cosa fa Adamo?

In questo mondo, ci sono due modi per giocare:

1. La strategia "storica": Eva guarda tutto il passato. "Ah, Adamo ha suonato tre 'Re' di fila, quindi ora devo suonare un 'Fa' per bilanciare." Questa strategia richiede una memoria enorme e un cervello molto complesso.
2. La strategia "posizionale" (o istantanea): Eva guarda solo la nota che sta suonando in questo preciso istante. Non le importa del passato. "Sono sulla nota 'Re', quindi la prossima deve essere 'Fa'." È come un semaforo: se è rosso, fermati; se è verde, vai. Niente storia, solo il presente.

La domanda fondamentale di questo articolo è: Per quali regole di gioco (quali "melodie" infinite) Eva può sempre vincere usando solo la strategia istantanea, senza bisogno di ricordare il passato?

Il Problema: Troppa Complessità

Fino a poco tempo fa, gli scienziati sapevano che per alcune regole semplici (come il "Parità", dove la nota più bassa suonata infinite volte deve essere pari) la strategia istantanea funziona. Ma per regole più complesse? Non c'era una mappa chiara. Era come cercare di navigare in una foresta senza bussola: sapevamo che alcuni sentieri erano sicuri, ma non sapevamo come riconoscere gli altri.

La Scoperta: La "Mappa della Posizionalità"

Gli autori, Antonio Casares e Pierre Ohlmann, hanno creato una mappa completa per le regole più comuni (quelle che possono essere descritte da macchine matematiche chiamate "automati a parità").

Hanno scoperto che una regola è "posizionale" (giocabile senza memoria) se e solo se l'automata che la descrive ha una struttura interna molto specifica, che chiamano "Automata a Firma".

Ecco l'analogia per capire cosa significa:
Immagina che l'automata sia un labirinto.

• In un labirinto normale, potresti dover ricordare se hai già passato un certo corridoio per non girare in tondo.
• In un "Labirinto a Firma", ogni stanza ha un'etichetta numerica (una "firma").
• La regola magica è: se sei in una stanza con un numero basso, puoi sempre trovare una via d'uscita che ti porta a una stanza con un numero ancora più basso, oppure ti mantiene su un numero pari che ti fa vincere.
• È come se il labirinto avesse una scala infinita che Eva può sempre scendere. Non importa quanto Adamo cerchi di confonderla, Eva può sempre dire: "Ok, sono qui, scendo di un gradino". Se riesce a scendere all'infinito o a fermarsi su un gradino "vincitore" (pari), allora vince.

Cosa ci dicono queste scoperte?

1. Possiamo controllare tutto velocemente (Decidibilità):
   Prima, per sapere se una regola era giocabile senza memoria, bisognava fare calcoli lunghissimi e complessi. Ora, grazie alla loro "mappa", possiamo controllare se una regola è giocabile in pochi secondi (tempo polinomiale), anche se la regola è molto complessa. È come avere un metal detector che ti dice subito se c'è un tesoro (una strategia semplice) o solo sassi.

2. Il trucco del "Salto nel Vuoto" (Lift):
   C'era un dubbio: "Se Eva sa vincere in giochi piccoli e finiti, sa vincere anche in giochi infiniti e giganteschi?"
   La risposta è SÌ. Se la strategia funziona per i giochi semplici, funziona anche per quelli infiniti. È come dire: "Se sai guidare in un parcheggio vuoto, sai guidare anche in un'autostrada trafficata" (per certe regole di guida). Questo risolve un enigma che gli scienziati si ponevano da anni.

3. Unire le regole (Unione):
   Immagina di avere due regole di vittoria: "Vinci se suoni 'Do' infinite volte" OPPURE "Vinci se suoni 'Re' infinite volte".
   Se entrambe le regole sono giocabili senza memoria, anche la loro combinazione lo è (con una piccola condizione). È come dire: se sai vincere a scacchi e sai vincere a dama, sai anche vincere a una partita mista scacchi-dama. Questo risolve una congettura famosa di Kopczyński.

4. La lettera "Invisibile" (Neutral Letter):
   Cosa succede se aggiungiamo una nota che non conta nulla (una nota "neutra") alla melodia? La loro ricerca conferma che se la regola originale era giocabile senza memoria, lo rimane anche con questa nota aggiuntiva. È come aggiungere un respiro in più a una frase: non cambia il significato, quindi la strategia per dirlo rimane la stessa.

Perché è importante?

Questo lavoro non è solo teoria astratta. È fondamentale per la sicurezza dei computer.
Quando progettiamo un sistema critico (come il software di un'auto a guida autonoma o il controllo di una centrale nucleare), vogliamo essere sicuri che il sistema possa reagire a qualsiasi imprevisto dell'ambiente (Adamo) senza dover memorizzare una storia infinita di eventi passati.

Se il sistema deve ricordare tutto il passato per prendere decisioni, diventa lento, costoso e soggetto a errori. Se invece può prendere decisioni basandosi solo sulla situazione attuale (strategia posizionale), il sistema è più robusto, più veloce e più facile da verificare.

In sintesi, gli autori hanno scritto il "manuale di istruzioni" definitivo per capire quando un sistema complesso può essere controllato in modo semplice e immediato, risolvendo molti dei grandi misteri rimasti aperti in questo campo per decenni.

Sommario tecnico

Ecco un riassunto tecnico dettagliato del paper "Positional 𝜔-regular languages" di Antonio Casares e Pierre Ohlmann, pubblicato su TheoretiCS nel 2026.

1. Il Problema

Il lavoro si inserisce nel contesto della teoria dei giochi su grafi a durata infinita, dove due giocatori antagonisti (Eve e Adam) muovono un token lungo i bordi di un grafo colorato. L'obiettivo di Eve è produrre un percorso infinito la cui sequenza di colori appartiene a una lingua specifica $W$ (l'obiettivo).

Il problema centrale affrontato è la complessità delle strategie: in particolare, si indaga se un obiettivo $W$ sia posizionale. Un obiettivo è detto posizionale se, in qualsiasi gioco che lo utilizza come condizione di vittoria, Eve può giocare in modo ottimale utilizzando una strategia posizionale (o memoriale). Una strategia posizionale dipende solo dal vertice corrente e non dalla storia del gioco.

Sebbene la biposizionalità (dove anche Adam può giocare in modo posizionale) sia ben compresa (caratterizzata da obiettivi di parità per obiettivi indipendenti dai prefissi), la posizionalità per un solo giocatore è stata storicamente più difficile da caratterizzare. Esistevano congetture aperte, come quella di Kopczyński sulla chiusura dell'unione di obiettivi posizionali, e la questione della decidibilità della posizionalità per le lingue $\omega$-regolari in tempo polinomiale.

2. Metodologia

Gli autori adottano un approccio basato sull'automata theory e sulla teoria dei grafi universali. La metodologia si articola in tre pilastri principali:

• Automati di Parità e Forme Normali: L'analisi si concentra sugli automi di parità deterministici che riconoscono le lingue $\omega$-regolari. Vengono utilizzati concetti avanzati come le forme normali degli automi, le congruenze e le preordini monotoni sugli stati.
• Grafi Universali: Si fa leva sulla caratterizzazione della posizionalità tramite l'esistenza di grafi universali monotoni ben ordinati (un risultato precedente di Ohlmann). Se esiste un grafo che può "mappare" qualsiasi gioco di una certa dimensione che soddisfa l'obiettivo, allora l'obiettivo è posizionale.
• Automati Storico-Deterministici (HD): Un contributo tecnico cruciale è l'uso sistematico degli automi storico-deterministici (o "good-for-games"). Questi automi, pur essendo non deterministici, permettono di risolvere le non-deterministicità passo-passo basandosi solo sulla storia del gioco, fungendo da ponte tra automi deterministici e strutture combinatorie come i grafi universali.

3. Contributi Chiave e Risultati

Il risultato principale è una caratterizzazione completa e sintattica della posizionalità per le lingue $\omega$-regolari, espressa nel Teorema 3.1.

A. Caratterizzazione Sintattica (Teorema 3.1)

Per una lingua $\omega$-regolare $W$, le seguenti affermazioni sono equivalenti:

1. $W$ è posizionale su giochi finiti privi di transizioni $\varepsilon$ controllati da Eve.
2. Esiste un automa di firma (signature automaton) deterministico, fully progress consistent, che riconosce $W$.
3. Esiste un automa di parità deterministico $\varepsilon$-completabile che riconosce $W$.
4. Per ogni cardinale $\kappa$, esiste un grafo ben ordinato e monotono $(\kappa, W)$-universale.
5. $W$ è posizionale su tutti i giochi (anche infiniti e con transizioni $\varepsilon$).

Definizioni Tecniche:

• Signature Automaton: Un automa dotato di una gerarchia di preordini totali sugli stati che rifiniscono l'inclusione dei residui linguistici e soddisfano proprietà di monotonia locale e separazione sicura.
• Full Progress Consistency: Una proprietà semantica che garantisce che se un percorso fa un "progresso" rispetto all'ordine degli stati (rispetto a un certo livello di priorità), la ripetizione infinita di quel percorso deve essere vincente.
• $\varepsilon$-Completable: La possibilità di aggiungere transizioni $\varepsilon$ (senza cambiare la lingua riconosciuta) per rendere l'automa completo rispetto a certi ordini totali sugli stati.

B. Conseguenze e Risoluzione di Congetture

Da questa caratterizzazione derivano diversi risultati fondamentali:

1. Decidibilità in Tempo Polinomiale: È possibile decidere in tempo polinomiale se un dato automa di parità deterministico riconosce una lingua posizionale (Teorema 3.2). Vengono proposti due algoritmi: uno basato sulla costruzione ricorsiva dell'automa di firma e uno basato sulla procedura di $\varepsilon$-completamento.
2. Lift Finite-to-Infinite e 1-to-2 Players:
   • Se un obiettivo $\omega$-regolare è posizionale su giochi finiti privi di $\varepsilon$ controllati da Eve, allora è posizionale su tutti i giochi (Teorema 3.3). Questo risponde positivamente a una congettura di Vandenhove.
   • La posizionalità su giochi a un giocatore implica la posizionalità su giochi a due giocatori per le lingue $\omega$-regolari.
3. Chiusura all'Unione (Congettura di Kopczyński): L'unione di due obiettivi $\omega$-regolari posizionali è posizionale, purché almeno uno dei due sia indipendente dai prefissi (Teorema 3.4). Questo risolve una versione rafforzata della congettura di Kopczyński nel caso $\omega$-regolare.
4. Aggiunta di Lettere Neutrali: Se $W$ è posizionale, anche l'obiettivo ottenuto aggiungendo una lettera neutra è posizionale (Teorema 3.9), risolvendo una congettura di Ohlmann per le lingue $\omega$-regolari.

C. Risultati Estesi

Il paper estende anche la caratterizzazione della biposizionalità a tutti gli obiettivi (non solo $\omega$-regolari), rimuovendo l'assunzione di indipendenza dai prefissi (Teorema 7.1). Inoltre, vengono fornite caratterizzazioni per obiettivi chiusi (safety) e aperti (reachability) su grafi arbitrari, introducendo il concetto di reset-stability.

4. Significato e Impatto

Questo lavoro rappresenta un punto di svolta nella teoria dei giochi su grafi e nella sintesi reattiva:

• Completezza Teorica: Fornisce la prima caratterizzazione sintattica completa per la posizionalità delle lingue $\omega$-regolari, colmando un vuoto di conoscenza durato decenni.
• Efficienza Algoritmica: Trasforma un problema di verifica di proprietà strutturali complesse in un algoritmo decisionale efficiente (tempo polinomiale), rendendo praticabile l'analisi di sistemi complessi.
• Strumenti Nuovi: Introduce strumenti tecnici innovativi come gli automi di firma e le tecniche di $\varepsilon$-completamento, che potrebbero trovare applicazione in altri ambiti della teoria degli automi (es. minimizzazione, apprendimento automatico).
• Risoluzione di Problemi Aperti: Risolve definitivamente la congettura di Kopczyński per la classe $\omega$-regolare e conferma l'ipotesi che la posizionalità su giochi finiti implichi quella su giochi infiniti per questa classe.

In sintesi, il paper non solo risolve problemi aperti fondamentali, ma offre un quadro unificato che collega la struttura degli automi, la teoria dei grafi universali e la complessità delle strategie, fornendo basi solide per futuri sviluppi nella sintesi di controller e nella verifica formale.