Omega automa
Un ω-automa o automa su parole infinite è, in informatica teorica e specialmente nella teoria degli automi, è un automa a stati finiti che accetta parole di lunghezza infinita.
Gli automi su parole infinite vengono utilizzati per modellare calcoli che non si completano, come il comportamento di un sistema operativo o di un sistema di controllo. Per tali sistemi, è possibile specificare proprietà come "ogni richiesta sarà seguita da una risposta" o la sua negazione "c'è una richiesta che non è seguita da una risposta" nell'ambito della verificazione di modelli (o model checking). Tali proprietà possono essere formulate per infinite parole e possono essere verificate da automi finiti.
Sono state introdotte diverse classi di automi su parole di lunghezza infinita: gli automi di Büchi, automi di Rabin, automi di Streett, automi a parità, automi di Muller e, per ogni classe, versioni deterministiche o non deterministiche. Queste classi differiscono solo nella loro condizione di accettazione. Tutte queste classi, con la notevole eccezione degli automi di Büchi deterministici, riconoscono la stessa famiglia di insiemi di parole infinite, chiamati insiemi regolari di parole infinite o linguaggi ω-regolari. Questi automi, anche se accettano gli stessi linguaggi, possono variare di dimensioni su uno specifico linguaggio.
Definizione
Quanto agli automi finiti, un automa su parole infinite su un alfabeto è dato da tale che
- è un insieme finito di stati,
- è l'insieme delle transizioni,
- è l'insieme degli stati iniziali,
- è un insieme di stati finali o terminali.
Spesso si assume che l'insieme degli stati iniziali sia composto da un singolo elemento. Una transizione è composta da uno stato di partenza , un'etichetta e uno stato di arrivo . Un calcolo (detto anche un percorso o una traccia) è una serie infinita di transizioni consecutive:
Per , lo stato iniziale è , la sua etichetta è la parola infinita . Il calcolo ha esito positivo e la parola viene accettata (o riconosciuta dall'automa) se passa infinitamente spesso attraverso uno stato terminale.
Un automa è detto deterministico se soddisfa le due condizioni seguenti:
- possiede un solo stato iniziale;
- per ogni stato e per ogni lettera , c'è al massimo una transizione che parte da e recante l'etichetta .
Condizione di accettazione
Per un calcolo , è l'insieme degli stati che compaiono un numero infinito di volte in . È questo concetto che permette di formulare le condizioni di accettazione.
Automi di Büchi
Template:Vedi anche La condizione di accettazione è: accetta una parola infinita se e solo se è l'etichetta di un calcolo per cui contiene almeno uno stato finale, quindi tale che .
Automa di Rabin
Un automa di Rabin è definito con un insieme di coppie di insiemi di stati . La condizione di accettazione è : accetta una parola infinita w se e solo se w è l'etichetta di un calcolo per il quale esiste una coppia di per la quale e .
Automa di Streett
Un automa di Streett è definito con un insieme di coppie di insiemi di stati . La condizione di accettazione è : accetta una parola infinita w se e solo se w è l'etichetta di un calcolo per il quale, per ogni coppia di , si ha e [1].
La condizione di Streett è la negazione della condizione di Rabin. Un automa di Streett deterministico accetta quindi esattamente il complemento dell'insieme accettato dall'automa di Rabin deterministico sullo stesso insieme .
Automa di parità
Un automa di parità è un automa i cui stati sono numerati. La condizione di accettazione è: accetta una parola infinita w se e solo se w è l'etichetta di un calcolo dove il più piccolo degli interi in è pari.
Automa di Muller
Un automa di Muller è definito con una famiglia di insiemi di stati. La condizione di accettazione è: accetta una parola infinita se e solo se è l'etichetta di un calcolo tale che .
Qualsiasi automa di Büchi può essere visto come un automa di Muller: basta prenderlo come tutti i sottoinsiemi di contenenti almeno uno stato terminale. Al contrario, per ogni automa di Muller a stati e insiemi di accettazione, esiste al massimo un automa di Büchi equivalente con al più stati. Allo stesso modo, gli automi di Rabin, Streett e parità possono essere visti come degli automi di Muller.
Potere espressivo
Un linguaggio di parole infinite o ω-language è un insieme di parole di lunghezza infinita su un dato alfabeto. Il potere espressivo di un ω-automa è misurato dalla classe di tutti i ω-linguaggi che possono essere riconosciuti dall'automa. Gli automi di Büchi, parità, Rabin, Streett e Muller non deterministici riconoscono tutti gli stessi linguaggi, che sono i linguaggi ω-regolari. Si può dimostrare che gli automi deterministici di parità, di Rabin, Streett e Muller riconoscono questi stessi linguaggi, diversamente dagli automi di Büchi deterministici. Ne consegue in particolare che la classe dei ω-linguaggi è chiusa dalla complementazione.
Esempio
L'automata in figura riconosce l'insieme di parole di lunghezza infinite sull'alfabeto composto da due lettere e che contengono un numero finito di lettere , cioè l'insieme . In effetti, per ogni parola del tipo , esiste un'esecuzione dell'automa che si ripete nello stato q, il quale è terminale.
Si dimostra che non esiste un automa di Büchi deterministico che accetta il linguaggio . Gli automi di Büchi deterministici sono strettamente meno espressivi degli automi di Büchi non deterministici[2].