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 ${\mathcal {A}}$ su un alfabeto $\Sigma$ è dato da ${\mathcal {A}}=(Q,{\mathcal {F}},I,T)$ tale che

$Q$ è un insieme finito di stati,
${\mathcal {F}}\subseteq Q\times \Sigma \times Q$ è l'insieme delle transizioni,
$I\subseteq Q$ è l'insieme degli stati iniziali,
$T\subseteq Q$ è un insieme di stati finali o terminali.

Spesso si assume che l'insieme degli stati iniziali sia composto da un singolo elemento. Una transizione $f=(p,a,q)\in {\mathcal {F}}$ è composta da uno stato di partenza $p$ , un'etichetta $a$ e uno stato di arrivo $q$ . Un calcolo $c$ (detto anche un percorso o una traccia) è una serie infinita di transizioni consecutive:

c=(p_{0},a_{1},p_{1})(p_{1},a_{2},p_{2})\cdots

Per $c$ , lo stato iniziale è $p_{0}$ , la sua etichetta è la parola infinita $a_{1}a_{2}\cdots a_{n}\cdots$ . 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 $q$ e per ogni lettera $a$ , c'è al massimo una transizione che parte da $q$ e recante l'etichetta $a$ .

Condizione di accettazione

Per un calcolo $c$ , ${\rm {Inf}}(c)$ è l'insieme degli stati che compaiono un numero infinito di volte in $c$ . È questo concetto che permette di formulare le condizioni di accettazione.

Automi di Büchi

La condizione di accettazione è: ${\mathcal {A}}$ accetta una parola infinita se e solo se è l'etichetta di un calcolo $c$ per cui ${\rm {Inf}}(c)$ contiene almeno uno stato finale, quindi tale che ${\rm {Inf}}(c)\cap T\neq \emptyset$ .

Automa di Rabin

Un automa di Rabin è definito con un insieme $\Omega$ di coppie di insiemi di stati $(E,F)$ . La condizione di accettazione è : ${\mathcal {A}}$ accetta una parola infinita w se e solo se w è l'etichetta di un calcolo per il quale esiste una coppia $(E,F)$ di $\Omega$ per la quale ${\rm {Inf}}(c)\cap E=\emptyset$ e ${\rm {Inf}}(c)\cap F\neq \emptyset$ .

Automa di Streett

Un automa di Streett è definito con un insieme $\Omega$ di coppie di insiemi di stati $(E,F)$ . La condizione di accettazione è : ${\mathcal {A}}$ accetta una parola infinita w se e solo se w è l'etichetta di un calcolo per il quale, per ogni coppia $(E,F)$ di $\Omega$ , si ha ${\rm {Inf}}(c)\cap E\neq \emptyset$ e ${\rm {Inf}}(c)\cap F=\emptyset$ ^[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 $\Omega$ .

Automa di parità

Un automa di parità è un automa i cui stati sono numerati. La condizione di accettazione è: ${\mathcal {A}}$ accetta una parola infinita w se e solo se w è l'etichetta di un calcolo dove il più piccolo degli interi in ${\rm {Inf}}(c)$ è pari.

Automa di Muller

Un automa di Muller è definito con una famiglia ${\mathcal {M}}$ di insiemi di stati. La condizione di accettazione è: ${\mathcal {A}}$ accetta una parola infinita se e solo se è l'etichetta di un calcolo tale che ${\rm {Inf}}(c)\subseteq {\mathcal {M}}$ .

Qualsiasi automa di Büchi può essere visto come un automa di Muller: basta prenderlo come ${\mathcal {M}}$ tutti i sottoinsiemi di $Q$ contenenti almeno uno stato terminale. Al contrario, per ogni automa di Muller a $n$ stati e $m$ insiemi di accettazione, esiste al massimo un automa di Büchi equivalente con al più $n+mn2^{n}$ 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

Automa di Büchi non déterministico che riconosce la parole infinite con un numero finito di

a

.

L'automata in figura riconosce l'insieme di parole di lunghezza infinite sull'alfabeto composto da due lettere $a$ e $b$ che contengono un numero finito di lettere $a$ , cioè l'insieme $\{a,b\}^{*}b^{\omega }$ . In effetti, per ogni parola del tipo $\{a,b\}^{*}b^{\omega }$ , 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 $\{a,b\}^{*}b^{\omega }$ . Gli automi di Büchi deterministici sono strettamente meno espressivi degli automi di Büchi non deterministici^[2].

Note

^ Farwer, p. 7.
^ Christel Baier e Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, 31 maggio 2008, pp. 191, 975, ISBN 978-0-262-02649-9.

Bibliografia

(EN) Berndt Farwer, ω-Automata, in Erich Grädel, Wolfgang Thomas e Thomas Wilke (a cura di), Automata logics, and infinite games: A guide to current research,, collana Lecture Notes in Computer Science, n. 2500, Springer-Verlag New York, Inc., 1º gennaio 2002, pp. 3-22, ISBN 978-3-540-00388-5.
(EN) Wolfgang Thomas, Automata on infinite objects, in Jan Van Leeuwen (a cura di), Handbook of Theoretical Computer Science: Formal Models and Semantics, t. B, MIT Press, 1990, pp. 133-192, ISBN 0-262-72015-9.
(EN) Dominique Perrin e Jean-Éric Pin, Infinite Words, Elsevier, 2004, p. 538, ISBN 978-0-12-532111-2.

Voci correlate

Collegamenti esterni

Paritosh K. Pandya, Automata on Infinite Words (PDF), su tcs.tifr.res.in.
Yann Pequignot, Automata, Languages and Logic (PDF), su hec.unil.ch, Federal Polytechnic School of Lausanne, 2009. URL consultato il 5 gennaio 2021 (archiviato dall'url originale il 3 marzo 2016).

Portale Informatica: accedi alle voci di Wikipedia che trattano di informatica

[1] Farwer, p. 7.

[2] Christel Baier e Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, 31 maggio 2008, pp. 191, 975, ISBN 978-0-262-02649-9.

[1]

[2]