V&V-Weak S1S

In questo articolo vedremo la definizione di Weak Second monadic Theory of One’s Successor e perchè ha senso parlarne.

Negli articoli precedenti avevamo visto alcune cose sui linguaggi $\omega$-regolari e come gli automi di Buchi fossero il top per riuscire a modellarli. Inoltre avevamo pure visto che dato un automa di Buchi $\cal{A}$ potevamo usare una formulazione $S1S_{\cal{A}}$ dipendente dall’alfabeto usato dall’automa. Da qui la necessità di usare la formulazione alfabeto-agnostica $S1S$ che non era niente più che una formulazione che convertiva qualsiasi alfabeto in un alfabeto binario.

L’ultima lezione poi era servita per dimostrare che un linguaggio $\omega$-regolare $L\subseteq A^\omega$ è $\omega$-regolare se e solo se è definibile in S1S (per il secondo teorema di Buchi).

Ma quindi che ci serve dire ancora? Bè, semplicemente il caro vecchio Buchi ha studiato anche quello che succede se le variabili del second’ordine sono limitate ad essere insiemi finiti. Dobbiamo immaginare che fino adesso le parole infinite erano computazioni di sistemi reattivi in cui volevamo analizzare certe proprietà. Per prima cosa abbiamo trovato un modo per rappresentare le computazioni tramite automa (e abbiamo quindi tirato fuori dal cappello gli automi di Buchi), poi abbiamo detto “questa forma forse è un po’ scomoda, meglio usare la logica che è un formalismo carino e coccoloso che è in voga da tipo 5000 anni” (e abbiamo tirato fuori S1S). Ora quello che vogliamo è tirare fuori dal cilindro un nuovo formalismo che ci permetta di rappresentare sistemi reattivi in cui certe proprietà valgono solo in certi frammenti di computazione. In parole povere vogliamo un formalismo che mi permetta di analizzare delle proprietà locali di una parola infinita.

Con S1S possiamo trattare problemi come “verifica che dopo ogni a ci siano solo delle b”

Con WS1S possiamo trattare i problemi come “verifiche dopo ogni a ci sia una certo numero di b”

Ma scusa, ma se vogliamo trattare delle proprietà locali perchè non “tagliamo” dalla sequenza infinita la porzione che ci serve e la analizziamo con uno dei tanti metodi che esistono per trattare le parole finite? Bè, perchè vogliamo un formalismo che gestisca le parole infinite e ne permetta di verificare alcune proprietà locali: semplice.