ω-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 a parità, 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.