Problema di Church

Il problema di Church chiede se, data una specifica logica della relazione tra sequenza di input e sequenza di output, sia possibile costruire automaticamente un sistema finito che produca l'output corretto per ogni input.

Idea

L'ambiente sceglie l'input, il sistema sceglie l'output. La soluzione cercata e' un automa di Mealy che realizzi una strategia vincente.

Soluzione di Buchi-Landweber

Per specifiche in S1S, la procedura passa attraverso:

S1S -> automa di Muller -> gioco di Muller -> gioco di parita -> automa di Mealy.

Se esiste una strategia vincente per il sistema, esiste anche una strategia a stati finiti costruibile effettivamente.

Collegamenti

• Automi di Mealy
• Automi di Muller
• Giochi di parità
• Secondo teorema di Büchi

Giochi di parita

Un gioco di parita e' un gioco infinito su grafo finito in cui ogni stato ha una priorita numerica.

Condizione di vittoria

Una run infinita e' vincente per un giocatore se la massima priorita vista infinitamente spesso ha la parita favorevole, spesso pari per il giocatore di sistema.

Importanza

I giochi di parita sono centrali nella sintesi e nel model checking del mu-calcolo. Le condizioni di Muller possono essere simulate tramite giochi di parita usando la LAR construction.

Strategie

I giochi di parita sono determinati e ammettono strategie posizionali vincenti.

Collegamenti

• Problema di Church
• Automi di Muller
• Registro di ultima apparizione (LAR)

Registro di ultima apparizione

Il registro di ultima apparizione (LAR) e' una memoria finita che registra l'ordine piu recente in cui sono comparsi gli stati di un gioco o di una run.

Uso

La costruzione LAR permette di trasformare una condizione di Muller, basata sull'insieme degli stati visitati infinitamente spesso, in una condizione di parita.

Collegamenti

• Automi di Muller
• Giochi di parità
• Problema di Church

Automi di Mealy

Un automa di Mealy e' una macchina a stati finiti che produce output in base allo stato corrente e al simbolo di input.

Forma generale

E' adatto a modellare controllori reattivi: a ogni passo legge un input dell'ambiente e produce immediatamente un output del sistema.

Uso nella sintesi

Nel problema di Church, la soluzione cercata e' un automa di Mealy che implementa una strategia vincente a memoria finita.

Collegamenti

• Problema di Church
• Trasduttori sequenziali

Approfondimento completo settimana 5 - Sintesi, giochi e Buchi-Landweber

Questa e' la versione estesa e autocontenuta del capitolo 10, nello stesso spirito del capitolo 9: ogni oggetto viene prima motivato, poi definito, poi riletto in parole. L'obiettivo e' saper ricostruire all'orale la pipeline completa:

specifica logica -> automa deterministico -> gioco -> strategia vincente -> automa di Mealy.

Di cosa parla davvero questo capitolo

Fino al capitolo 9 il problema principale era:

$$M\models\varphi?$$

cioe': dato un modello $M$ gia' costruito, verificare se soddisfa una specifica $\varphi$.

Il capitolo 10 cambia domanda:

data una specifica, posso costruire automaticamente un sistema finito che la soddisfa?

Questa e' la sintesi. Non controlliamo piu' un sistema gia' dato: proviamo a costruire il controllore stesso.

Il capitolo segue la formulazione classica del problema di Church e la soluzione di Buchi-Landweber. Gli strumenti sono tutti gia' comparsi nei capitoli precedenti, ma qui vengono collegati in una catena nuova:

1. la logica S1S descrive la relazione desiderata fra input e output;
2. il teorema di Buchi trasforma la formula in un automa su parole infinite;
3. la determinizzazione porta a un automa deterministico di Muller;
4. l'automa viene trasformato in un gioco fra ambiente e sistema;
5. il gioco viene risolto tramite condizioni Muller/parita;
6. una strategia vincente viene implementata come automa di Mealy.

La mappa del capitolo e':

1. Parte I: perche' la sintesi non e' model checking.
2. Parte II: il problema di Church, online e finite-state.
3. Parte III: automi di Mealy come controllori.
4. Parte IV: da S1S ad automi deterministici di Muller.
5. Parte V: da automi a giochi.
6. Parte VI: strategie, regioni vincenti e determinazione.
7. Parte VII: reachability, weak Muller, Muller.
8. Parte VIII: LAR e giochi di parita.
9. Parte IX: soluzione completa di Church's problem.
10. Parte X: errori tipici, esercizi e mappa per l'orale.

0. Richiami minimi

S1S. E' la logica monadica del secondo ordine su $(\omega,+1)$. Serve a parlare di posizioni naturali e di insiemi di posizioni. Una parola binaria infinita si puo' rappresentare come un insieme $X\subseteq\omega$: $i\in X$ vuol dire che alla posizione $i$ il bit vale 1.

Automi su parole infinite. Gli automi di Buchi/Muller leggono sequenze infinite. La condizione di accettazione non riguarda uno stato finale "alla fine", perche' non c'e' fine: riguarda cio' che accade infinitamente spesso.

Automa deterministico di Muller. Un automa di Muller ha una famiglia $\mathcal{F}\subseteq 2^Q$ e accetta una run $\rho$ se:

$$Inf(\rho)\in\mathcal{F}.$$

Qui $Inf(\rho)$ e' l'insieme degli stati visitati infinitamente spesso.

Gioco infinito. Un gioco su grafo finito produce una play infinita. Alcuni stati sono controllati dall'ambiente, altri dal sistema. Una winning condition decide se la play e' vinta dal sistema.

Automa di Mealy. E' una macchina finita che legge input e produce output. Nel capitolo 10 e' il formato finale del controllore sintetizzato.

Parte I - Dal model checking alla sintesi

1. Il limite concettuale del model checking

Il model checking e' potente, ma parte da un presupposto:

il modello del sistema esiste gia'.

L'algoritmo prende:

$$K=(S,S_0,R,L)$$

e una formula temporale $\varphi$, poi risponde se:

$$K\models\varphi.$$

Se la risposta e' negativa, abbiamo un controesempio. Se e' positiva, sappiamo che il modello rispetta la specifica.

Ma restano due problemi pratici.

Primo problema: il modello puo' essere sbagliato. Un controesempio puo' indicare un bug reale, ma puo' anche indicare che il modello non rappresenta bene il sistema che volevamo costruire.

Secondo problema: il sistema reale va ancora implementato. Anche se il modello e' corretto, bisogna trasformarlo in codice, circuito, controllore o protocollo. In questa trasformazione si possono introdurre errori.

La sintesi nasce per eliminare questo passaggio:

invece di costruire a mano un sistema e poi verificarlo, costruiamolo automaticamente dalla specifica.

2. Che cosa significa "sintesi" in questo capitolo

La parola sintesi puo' indicare cose diverse. Gli appunti chiariscono che qui non si parla genericamente di "trovare un modello" per una formula.

Qui sintesi significa:

costruire un controllore finito che interagisce con un ambiente e soddisfa una specifica per ogni comportamento possibile dell'ambiente.

Il controllore non sceglie tutto. L'ambiente fornisce input. Il sistema produce output. La specifica dice quali coppie input/output sono accettabili.

Schema mentale:

Questa distinzione e' fondamentale: il sistema controlla $\beta$, non $\alpha$.

3. Perche la sintesi e' piu' forte della soddisfacibilita'

Una specifica puo' dire:

$$\varphi(X,Y)$$

dove:

• $X$ rappresenta l'input;
• $Y$ rappresenta l'output.

La soddisfacibilita' chiede:

$$\exists X\exists Y.\ \varphi(X,Y).$$

Lettura:

esiste almeno una coppia input/output buona?

La sintesi chiede qualcosa di molto piu' forte:

per ogni input scelto dall'ambiente, il sistema sa produrre online un output che soddisfa la specifica?

Una formula piu' vicina sarebbe:

$$\forall X\exists Y.\ \varphi(X,Y),$$

ma anche questa non basta, perche' manca il vincolo operativo:

• $Y$ deve dipendere causalmente da $X$;
• $Y(t)$ non puo' usare input futuri;
• la dipendenza deve essere implementabile da una macchina finita.

Quindi la sintesi non e' solo logica dei quantificatori. E' logica piu' causalita' piu' memoria finita.

4. Il punto di vista del gioco

La forma:

$$\forall X\exists Y$$

suggerisce gia' un gioco:

1. l'ambiente sceglie l'input;
2. il sistema risponde con l'output;
3. la specifica decide chi ha vinto.

Il sistema non deve trovare un singolo output buono per un singolo input. Deve avere una regola che funziona contro tutti gli input.

Questa regola e' una strategia.

Per questo il capitolo passa dai linguaggi e dagli automi ai giochi:

una soluzione della sintesi e' una strategia vincente del sistema.

5. Perche in generale la sintesi e' difficile

In generale, sintetizzare programmi da specifiche arbitrarie e' troppo potente. Il problema diventa indecidibile.

Il risultato positivo del capitolo e':

restringendo la specifica a S1S, il problema di Church e' decidibile.

Il prezzo e' alto: le costruzioni sono complesse e possono esplodere. Ma dal punto di vista teorico il risultato e' enorme:

• dice quando la sintesi e' possibile;
• dice come decidere se una soluzione esiste;
• dice come costruire una macchina finita quando esiste.

Parte II - Church's Problem

6. Formulazione informale

Il problema di Church riguarda trasformazioni fra sequenze infinite.

L'ambiente produce una sequenza di input:

$$\alpha=\alpha(0)\alpha(1)\alpha(2)\ldots$$

Il sistema produce una sequenza di output:

$$\beta=\beta(0)\beta(1)\beta(2)\ldots$$

La specifica descrive quali coppie:

$$(\alpha,\beta)$$

sono ammesse.

La domanda e':

data la specifica della relazione input/output, esiste una macchina finita che produce $\beta$ online per ogni $\alpha$, in modo che la coppia $(\alpha,\beta)$ soddisfi la specifica?

7. La parola "bit-to-bit"

Nella formulazione classica, Church's problem parla di trasformazioni bit-to-bit.

Vuol dire che a ogni istante:

• l'ambiente fornisce un bit;
• il sistema produce un bit.

Al tempo $t$:

$$\alpha(t)\in\{0,1\},\qquad \beta(t)\in\{0,1\}.$$

La coppia globale e' quindi una parola infinita su coppie:

$$((\alpha(0),\beta(0)),(\alpha(1),\beta(1)),\ldots) \in(\{0,1\}\times\{0,1\})^\omega.$$

Questa osservazione sara' importante quando costruiremo l'automa: l'automa legge coppie input/output.

8. La parola "online"

Online significa:

l'output corrente non puo' dipendere da input futuri.

Al tempo $t$, il sistema ha visto solo:

$$\alpha(0),\ldots,\alpha(t).$$

Quindi puo' produrre $\beta(t)$ usando il prefisso corrente, ma non $\alpha(t+1)$.

Esempio non realizzabile online:

$$\beta(t)=\alpha(t+1).$$

Per produrre $\beta(t)$ dovrei conoscere il prossimo input. Un controllore reale non puo' farlo.

Esempio realizzabile online:

$$\beta(t)=\alpha(t).$$

Qui il sistema copia l'input corrente. Non serve conoscere il futuro.

9. La parola "finite-state"

Finite-state significa:

tutta l'informazione rilevante del passato deve essere compressa in uno stato finito.

Il sistema non puo' ricordare un prefisso arbitrariamente lungo dell'input.

Esempio non finite-state:

al tempo $t$, produrre il numero esatto di 1 comparsi finora nell'input.

Se il numero deve essere esatto e illimitato, serve memoria non limitata.

Esempio finite-state:

produrre 1 se finora il numero di 1 visti e' pari, 0 se e' dispari.

Qui basta ricordare una parita', cioe' due stati.

10. Formalizzazione con S1S

Per una parola binaria infinita $\alpha$, definiamo:

$$P_\alpha=\{i\in\omega\mid \alpha(i)=1\}.$$

Allo stesso modo:

$$P_\beta=\{i\in\omega\mid \beta(i)=1\}.$$

Una specifica S1S:

$$\varphi(X,Y)$$

parla di due insiemi di posizioni:

• $X$ = posizioni in cui l'input vale 1;
• $Y$ = posizioni in cui l'output vale 1.

La coppia $(\alpha,\beta)$ soddisfa la specifica se:

$$(\omega,+1)\models \varphi[P_\alpha,P_\beta].$$

Quindi Church's problem diventa:

data $\varphi(X,Y)$, costruire un automa di Mealy che per ogni input $\alpha$ produce un output $\beta$ tale che $(\omega,+1)\models \varphi[P_\alpha,P_\beta]$, oppure dire che non esiste.

11. Lettura della quantificazione corretta

La specifica non chiede:

$$\exists P_\alpha\exists P_\beta.\ \varphi(P_\alpha,P_\beta).$$

Questa formula dice solo che esiste una coppia buona.

La specifica di realizzabilita' chiede:

esiste una funzione causale finita $F$ tale che per ogni input $\alpha$, l'output $\beta=F(\alpha)$ soddisfa $\varphi$?

In simboli, informalmente:

$$\exists F\ \forall \alpha.\ \varphi(P_\alpha,P_{F(\alpha)}).$$

Ma $F$ non e' una funzione arbitraria: deve essere una macchina finita online.

Questo e' il ponte con gli automi di Mealy.

Parte III - Automi di Mealy come controllori

12. Definizione di automa di Mealy

Un automa di Mealy e':

$$\mathcal{M}=(S,\Sigma,\Gamma,\delta,\tau,s_0).$$

Dove:

• $S$ e' l'insieme finito degli stati interni;
• $\Sigma$ e' l'alfabeto di input;
• $\Gamma$ e' l'alfabeto di output;
• $\delta:S\times\Sigma\to S$ aggiorna lo stato;
• $\tau:S\times\Sigma\to\Gamma$ produce l'output;
• $s_0$ e' lo stato iniziale.

Al tempo $t$, se lo stato interno e' $s_t$ e arriva input $\alpha(t)$, allora:

$$\beta(t)=\tau(s_t,\alpha(t))$$

e:

$$s_{t+1}=\delta(s_t,\alpha(t)).$$

13. Come si legge questa definizione

La funzione $\tau$ risponde alla domanda:

che output devo produrre adesso?

La funzione $\delta$ risponde alla domanda:

che cosa devo ricordare per il futuro?

Quindi un Mealy automaton e' esattamente un controllore online:

• legge input uno alla volta;
• produce output subito;
• aggiorna memoria finita.

14. Perche non basta un automa accettatore

Un automa accettatore legge una parola e alla fine, o secondo una condizione omega, decide se accettarla.

Nel problema di Church il sistema deve costruire la parola di output mentre legge l'input.

Quindi serve una macchina con output:

$$\tau:S\times\Sigma\to\Gamma.$$

Gli automi accettatori servono nella parte intermedia, per riconoscere le coppie input/output corrette. Il risultato finale, pero', deve essere un Mealy.

15. Strategia e Mealy sono la stessa idea vista da due lati

Nel gioco, una strategia dice:

se la storia finora e' questa, fai questa mossa.

Nel Mealy, lo stato interno riassume la storia, e $\tau$ dice che output produrre.

Quindi:

$$\text{strategia a memoria finita} \quad\Longleftrightarrow\quad \text{automa di Mealy}.$$

Questa equivalenza e' il motivo per cui i giochi sono utili alla sintesi.

16. Esempio piccolo: parita degli input

Specifica:

l'output deve essere 1 esattamente quando il numero di 1 visti finora nell'input e' dispari.

Bastano due stati:

• $E$: finora ho visto un numero pari di 1;
• $O$: finora ho visto un numero dispari di 1.

Transizioni:

Qui la memoria finita e' sufficiente perche' non serve ricordare il conteggio esatto, ma solo la sua parita'.

Parte IV - Da S1S ad automi deterministici di Muller

17. Perche compare un automa

S1S e automi su parole infinite sono collegati dal secondo teorema di Buchi:

i linguaggi definibili in S1S sono esattamente quelli riconoscibili da automi su parole infinite.

Data:

$$\varphi(X,Y),$$

costruiamo un automa che legge la parola infinita di coppie:

$$((\alpha(0),\beta(0)),(\alpha(1),\beta(1)),\ldots).$$

L'automa accetta esattamente le coppie input/output che soddisfano la formula.

18. Alfabeto dell'automa

Nel caso binario, l'alfabeto e':

$$\Sigma_\text{pair}=\{0,1\}\times\{0,1\}.$$

Una lettera e' una coppia:

$$(b,c)$$

dove:

• $b$ e' il bit scelto dall'ambiente;
• $c$ e' il bit scelto dal sistema.

Se l'automa legge una parola su questo alfabeto, sta leggendo insieme input e output.

19. Perche serve determinismo

Nel model checking automata-theoretic potevamo usare automi nondeterministici: se esisteva una run accettante, la parola era accettata.

Nella sintesi, pero', vogliamo trasformare l'automa in un gioco. Il gioco deve sapere in quale stato si trova dopo ogni coppia input/output.

Se l'automa fosse nondeterministico, ci sarebbe un'ulteriore scelta:

quale transizione nondeterministica prende l'automa?

Questa scelta non appartiene ne' all'ambiente ne' al sistema. Introdurla confonderebbe il gioco.

Per questo si usa un automa deterministico.

20. Perche Muller

Gli automi di Buchi deterministici non riconoscono tutti gli omega-linguaggi regolari. Per recuperare tutta l'espressivita' in forma deterministica, si usano condizioni piu' ricche, come Muller.

Un automa deterministico di Muller e':

$$\mathcal{A}=(Q,q_0,\Sigma,\delta,\mathcal{F})$$

con:

$$\mathcal{F}\subseteq 2^Q.$$

Dato un input infinito, l'automa produce una run unica:

$$\rho=q_0q_1q_2\ldots$$

e accetta se:

$$Inf(\rho)\in\mathcal{F}.$$

Lettura:

guardo quali stati appaiono infinitamente spesso; se quell'insieme appartiene alla famiglia vincente $\mathcal{F}$, la parola e' accettata.

21. Perche la condizione di Muller e' naturale per la sintesi

In una computazione reattiva non conta solo raggiungere qualcosa una volta. Spesso conta cio' che succede per sempre:

• una richiesta deve essere servita infinite volte;
• un errore deve non comparire mai da un certo punto in poi;
• certi stati devono ricorrere;
• certi stati devono sparire.

La condizione:

$$Inf(\rho)\in\mathcal{F}$$

e' molto generale proprio perche' parla della parte ricorrente della run.

Quando passeremo ai giochi, la stessa idea diventera':

il sistema vince se l'insieme degli stati visitati infinitamente spesso dalla partita appartiene a $\mathcal{F}$.

22. La pipeline fino a qui

Abbiamo trasformato:

$$\varphi(X,Y)$$

in:

$$\mathcal{A}_\varphi=(Q,q_0,\{0,1\}\times\{0,1\},\delta,\mathcal{F}).$$

Questo automa riconosce tutte e sole le coppie input/output corrette.

Ma non abbiamo ancora costruito un controllore. L'automa dice:

questa coppia completa e' accettabile.

La sintesi richiede:

il sistema puo' scegliere gli output in modo da rendere accettabile la coppia qualunque siano gli input?

Per rispondere serve un gioco.

Parte V - Da automa a gioco

23. Separare input e output

L'automa deterministico legge una coppia:

$$(b,c).$$

Ma nella sintesi i due componenti della coppia non sono scelti dallo stesso giocatore:

• $b$ lo sceglie l'ambiente;
• $c$ lo sceglie il sistema.

Quindi ogni passo dell'automa viene spezzato in due mosse.

Se l'automa e' nello stato $q$:

1. l'ambiente sceglie input $b$;
2. il gioco passa allo stato intermedio $(q,b)$;
3. il sistema sceglie output $c$;
4. l'automa avanza a:

$$q'=\delta(q,(b,c)).$$

Questa e' la costruzione centrale.

24. Stati del gioco

Partendo dall'automa di Muller, il gioco ha due tipi di stati.

Stati dell'ambiente. Sono gli stati originali dell'automa:

$$q\in Q.$$

In questi stati tocca all'ambiente scegliere il prossimo input.

Stati del sistema. Sono coppie:

$$(q,b)$$

dove $q$ e' lo stato dell'automa e $b$ e' l'input appena scelto.

In questi stati tocca al sistema scegliere l'output.

Quindi l'arena separa cio' che nell'automa era compresso in una singola lettera.

25. Archi del gioco

Da uno stato ambiente $q$ ci sono archi verso:

$$(q,0),\qquad(q,1).$$

Questi rappresentano le due possibili scelte dell'ambiente.

Da uno stato sistema $(q,b)$ ci sono archi verso:

$$\delta(q,(b,0)),\qquad \delta(q,(b,1)).$$

Questi rappresentano le due possibili scelte di output del sistema.

La partita alterna quindi:

$$q_0,\ (q_0,b_0),\ q_1,\ (q_1,b_1),\ q_2,\ldots$$

dove:

$$q_{i+1}=\delta(q_i,(b_i,c_i)).$$

26. Winning condition del gioco

La condizione di Muller dell'automa era:

$$Inf(q_0q_1q_2\ldots)\in\mathcal{F}.$$

Nel gioco compaiono anche gli stati intermedi $(q,b)$. Ci sono due modi equivalenti di pensarla:

1. proiettare la play sugli stati originali $Q$;
2. estendere la condizione ai nuovi stati in modo coerente.

Concettualmente, quello che conta e':

la coppia input/output generata dalla partita deve essere accettata dall'automa della specifica.

Quindi il sistema vince se la run dell'automa soddisfa la condizione di Muller.

27. Perche questa costruzione e' corretta

Ogni partita determina:

• una sequenza di input $\alpha$ scelta dall'ambiente;
• una sequenza di output $\beta$ scelta dal sistema;
• una run unica dell'automa deterministico sulla coppia $(\alpha,\beta)$.

Se il sistema ha una strategia vincente, allora qualunque sia $\alpha$, l'output prodotto dalla strategia genera una coppia accettata dall'automa.

Questo significa:

$$(\omega,+1)\models\varphi[P_\alpha,P_\beta].$$

Viceversa, un controllore Mealy che realizza la specifica induce una strategia vincente nel gioco: quando tocca al sistema, il controllore sceglie l'output.

28. Stati del gioco e stati del Mealy: non confonderli

Gli appunti insistono su questo punto:

gli stati del game graph non sono automaticamente gli stati del Mealy finale.

Il game graph e' l'arena:

• contiene stati dell'automa;
• contiene stati intermedi dopo la scelta dell'ambiente;
• serve a definire la partita.

Il Mealy finale deve implementare una strategia. I suoi stati devono contenere la memoria necessaria per decidere gli output.

Questa memoria puo' includere:

• lo stato corrente dell'automa di Muller;
• la memoria della strategia vincente;
• eventualmente memoria LAR o memoria derivata dal gioco di parita.

Quindi il Mealy finale nasce dal gioco, ma non coincide semplicemente con il grafo del gioco.

Parte VI - Giochi infiniti

29. Game graph

Un game graph, o arena, e':

$$G=(Q,Q_A,E).$$

Dove:

• $Q$ e' l'insieme finito degli stati;
• $Q_A\subseteq Q$ sono gli stati controllati dal giocatore A;
• $Q_B=Q\setminus Q_A$ sono gli stati controllati dal giocatore B;
• $E\subseteq Q\times Q$ e' la relazione degli archi.

Nel capitolo:

• A = ambiente;
• B = sistema.

Si assume che non ci siano deadlock:

$$\forall q\in Q,\quad \exists q'.\ (q,q')\in E.$$

Le partite sono infinite, come le computazioni reattive.

30. Play

Una play da $q_0$ e' un cammino infinito:

$$\rho=q_0q_1q_2\ldots$$

tale che:

$$(q_i,q_{i+1})\in E$$

per ogni $i$.

Quando $q_i\in Q_A$, sceglie A. Quando $q_i\in Q_B$, sceglie B.

Una play e' quindi una storia completa dell'interazione fra ambiente e sistema.

31. Winning condition

Un gioco e':

$$(G,W)$$

dove:

$$W\subseteq Q^\omega$$

e' l'insieme delle play vinte da B.

Se:

$$\rho\in W,$$

vince B. Altrimenti vince A.

Nel problema di Church:

• B vince = il sistema soddisfa la specifica;
• A vince = l'ambiente riesce a falsificarla.

32. Strategie

Una strategia per B e' una funzione che, ogni volta che la play arriva in uno stato di B, sceglie il prossimo stato.

Formalmente, una strategia generale puo' avere tipo:

$$f:Q^+\to Q.$$

Dato un prefisso:

$$q_0q_1\ldots q_k,$$

se $q_k\in Q_B$, la strategia sceglie un successore legale:

$$(q_k,f(q_0\ldots q_k))\in E.$$

33. Strategia vincente

Una strategia di B e' vincente da $q$ se:

qualunque cosa faccia A, ogni play che parte da $q$ e segue la strategia di B appartiene a $W$.

Questa e' la quantificazione giusta per la sintesi:

• il sistema controlla solo le proprie mosse;
• l'ambiente puo' scegliere qualsiasi input;
• la strategia deve funzionare contro tutte le scelte dell'ambiente.

34. Winning regions

La winning region di B e':

$$W_B=\{q\in Q\mid B\text{ ha una strategia vincente da }q\}.$$

La winning region di A e':

$$W_A=\{q\in Q\mid A\text{ ha una strategia vincente da }q\}.$$

Se:

$$W_A\cup W_B=Q,$$

il gioco e' determinato.

Lettura:

da ogni stato, uno dei due giocatori puo' forzare la vittoria.

Determinato non vuol dire facile da risolvere. Vuol dire che non esistono stati neutri in cui nessuno dei due abbia una strategia vincente.

35. Strategie posizionali e strategie a memoria finita

Una strategia posizionale dipende solo dallo stato corrente:

$$f(q).$$

Non ricorda la storia.

Una strategia a memoria finita ha uno stato interno finito. Aggiorna questa memoria lungo la play e usa la memoria per decidere.

Questa distinzione sara' essenziale:

Il trucco LAR serve proprio a trasformare memoria Muller in stato del gioco simulato, cosi' nel parity game bastano strategie posizionali.

Parte VII - Reachability, weak Muller, Muller

36. Reachability games

Dato un insieme target:

$$F\subseteq Q,$$

B vince se la play visita almeno una volta uno stato di $F$:

$$\exists i.\ \rho(i)\in F.$$

Questa e' la condizione piu' semplice:

raggiungi il target almeno una volta.

37. Attractor per reachability

La regione vincente di B si calcola con l'attrattore.

Si parte da:

$$Attr_B^0(F)=F.$$

Poi si ripete:

• aggiungi uno stato di B se ha almeno un successore gia' nell'attrattore;
• aggiungi uno stato di A se tutti i suoi successori sono gia' nell'attrattore.

Formula concettuale:

$$ Attr_B^{i+1}(F)=Attr_B^i(F) \cup \{q\in Q_B\mid \exists q'.\ qEq'\land q'\in Attr_B^i(F)\} $$

$$ \cup \{q\in Q_A\mid \forall q'.\ qEq'\Rightarrow q'\in Attr_B^i(F)\}. $$

Si itera fino a stabilizzazione.

Lettura:

• se tocca a B, basta una mossa buona;
• se tocca ad A, tutte le mosse devono essere buone, perche' A e' avversario.

38. Perche reachability ha strategie posizionali

Quando uno stato entra nell'attrattore, entra con una "ragione":

• e' target;
• oppure B puo' andare verso uno stato piu' vicino al target;
• oppure A non puo' evitare di andare verso l'attrattore.

La strategia di B e':

in ogni stato di B, scegli un successore che diminuisce il livello dell'attrattore.

Non serve ricordare come ci si e' arrivati. Basta lo stato corrente.

39. Weak Muller games

Una condizione weak Muller, o Staiger-Wagner, guarda l'insieme degli stati visitati almeno una volta:

$$Occ(\rho)=\{q\in Q\mid \exists i.\ \rho(i)=q\}.$$

B vince se:

$$Occ(\rho)\in\mathcal{F}.$$

Questa condizione e' "weak" perche' non distingue fra:

• stati visitati una sola volta;
• stati visitati infinite volte.

Conta solo se sono comparsi.

40. Perche weak Muller puo' richiedere memoria

Se l'obiettivo riguarda l'insieme degli stati gia' visitati, il sistema puo' dover ricordare quali stati ha visto.

Esempio:

B vince se durante la play vengono visitati tutti gli stati di $\{1,2,3\}$.

Se B e' in una posizione con piu' scelte, potrebbe dover sapere quali stati mancano ancora. Una strategia che guarda solo lo stato corrente puo' non bastare.

Una memoria naturale e':

$$R\subseteq Q$$

dove $R$ e' l'insieme degli stati visitati finora.

Aggiornamento:

$$R' = R\cup\{q\}.$$

Questa memoria ha al massimo:

$$2^{|Q|}$$

valori.

41. Weak Muller come weak parity

Per weak Muller si puo' colorare ogni memoria $R$ in base a due informazioni:

• quanto e' grande $R$;
• se $R\in\mathcal{F}$.

Una codifica possibile:

$$c(R)=2|R|\quad\text{se }R\in\mathcal{F},$$

$$c(R)=2|R|-1\quad\text{se }R\notin\mathcal{F}.$$

Poiche' $R$ cresce monotonicamente e poi si stabilizza, il colore finale dice se l'insieme visitato appartiene a $\mathcal{F}$.

Questa e' una versione piu' semplice dell'idea che useremo per Muller pieno.

42. Muller games

Una condizione di Muller guarda:

$$Inf(\rho)=\{q\in Q\mid q\text{ appare infinitamente spesso in }\rho\}.$$

B vince se:

$$Inf(\rho)\in\mathcal{F}.$$

Questa e' piu' espressiva della weak Muller, perche' distingue:

• stati visitati solo finitely many times;
• stati visitati infinitely often.

Esempio:

$$\rho=a,b,c,b,c,b,c,\ldots$$

Allora:

$$Occ(\rho)=\{a,b,c\},$$

ma:

$$Inf(\rho)=\{b,c\}.$$

Weak Muller e Muller possono quindi dare risposte diverse.

43. Teorema sui Muller games

Il risultato usato nel capitolo e':

i Muller games su grafi finiti sono determinati; le winning regions sono calcolabili; il giocatore vincente ha una strategia a memoria finita.

Se il grafo ha $n$ stati, una costruzione standard usa memoria dell'ordine:

$$n!\cdot n.$$

Questa quantita' non e' casuale:

• $n!$ corrisponde agli ordini possibili degli stati;
• $n$ corrisponde alla posizione di hit nella costruzione LAR.

44. Game simulation

L'idea di game simulation e':

trasformare un gioco difficile in un gioco piu' semplice, preservando chi vince.

Dire che un gioco $(G,W)$ e' simulato da $(G',W')$ significa che una play $\rho$ di $G$ viene trasformata in una play $\rho'$ di $G'$ in modo che:

$$\rho\in W \quad\Longleftrightarrow\quad \rho'\in W'.$$

Perche' serve?

Se il gioco simulato $G'$ ha strategie posizionali, allora riportandole indietro otteniamo strategie a memoria finita per il gioco originale.

La costruzione:

$$\text{Muller}\to\text{parity}$$

tramite LAR e' esattamente una game simulation.

Parte VIII - LAR e giochi di parita

45. Latest Appearance Record

Il Latest Appearance Record registra l'ordine delle ultime apparizioni degli stati visitati.

Un LAR ha forma:

$$((i_1,\ldots,i_r),h).$$

Dove:

• $(i_1,\ldots,i_r)$ e' una lista di stati visti;
• gli stati piu' recenti stanno piu' a sinistra;
• $h$ e' la posizione di hit;
• $h=0$ quando lo stato letto e' nuovo.

Quando compare uno stato gia' presente nella lista:

1. si guarda la posizione in cui stava;
2. quella posizione diventa $h$;
3. lo stato viene spostato in testa.

46. Aggiornamento LAR: esempio base

Sequenza:

$$A,C,C,D,B,D,C,D,\ldots$$

Aggiorniamo la lista:

Il LAR non conserva tutta la storia. Conserva solo un ordine recente abbastanza informativo per recuperare la parte ricorrente.

47. Hitting set

Dato:

$$((i_1,\ldots,i_r),h)$$

con $h>0$, l'hitting set e':

$$H=\{i_1,\ldots,i_h\}.$$

Lettura:

quando uno stato ricompare, l'hitting set contiene gli stati attraversati dall'ultima apparizione di quello stato fino ad ora, secondo l'ordine LAR.

Nel limite infinito, gli hit che ricorrono infinitamente spesso rivelano quali stati ricorrono infinitamente spesso nella play.

48. Da Muller a colori

La condizione di Muller e':

$$Inf(\rho)\in\mathcal{F}.$$

Vogliamo tradurla in una condizione di parita sui LAR.

Per $h=0$ si puo' usare colore 0.

Per $h>0$:

$$c((i_1,\ldots,i_r),h)=2h \quad\text{se }\{i_1,\ldots,i_h\}\in\mathcal{F},$$

$$c((i_1,\ldots,i_r),h)=2h-1 \quad\text{se }\{i_1,\ldots,i_h\}\notin\mathcal{F}.$$

Quindi:

• hitting set buono -> colore pari;
• hitting set cattivo -> colore dispari.

La condizione di parita dice:

guarda il massimo colore che compare infinitamente spesso; se e' pari, vince B; se e' dispari, vince A.

49. Perche il massimo colore ricorrente funziona

In una play infinita, dopo un certo punto:

• gli stati visitati solo finitely many times spariscono;
• restano solo gli stati visitati infinitely often.

Il LAR continua allora a riorganizzare soprattutto gli stati ricorrenti.

Il massimo hit che compare infinitamente spesso corrisponde al blocco degli stati ricorrenti. Il suo hitting set coincide con:

$$Inf(\rho).$$

Quindi controllare se quell'hitting set appartiene a $\mathcal{F}$ equivale a controllare la condizione di Muller originale.

La parita del colore codifica esattamente questa appartenenza.

50. Esempio LAR completo

Sia:

$$Q=\{1,2,3\}$$

e:

$$\mathcal{F}=\{\{2,3\}\}.$$

B vince solo se gli stati visitati infinitamente spesso sono esattamente $\{2,3\}$.

Partita 1:

$$1,2,3,2,3,2,3,\ldots$$

Qui:

$$Inf(\rho)=\{2,3\}\in\mathcal{F}.$$

Traccia:

Da un certo punto in poi il colore ricorrente massimo e' 4, pari. Quindi B vince.

Partita 2:

$$1,2,3,1,2,3,1,2,3,\ldots$$

Qui:

$$Inf(\rho)=\{1,2,3\}\notin\mathcal{F}.$$

Traccia:

Il massimo colore ricorrente e' 5, dispari. Quindi B perde.

51. Parity games

Un parity game e' un gioco su grafo finito con una funzione colore:

$$c:Q\to\{0,\ldots,k\}.$$

Una play produce una sequenza infinita di colori:

$$c(q_0)c(q_1)c(q_2)\ldots$$

B vince se il massimo colore visto infinitamente spesso e' pari.

Questa e' la convenzione usata qui. Alcuni testi usano il minimo colore o invertono pari/dispari: il concetto non cambia, basta essere coerenti.

52. Perche i parity games sono comodi

I parity games sono comodi per tre motivi:

1. sono determinati;
2. ammettono strategie posizionali;
3. sono risolvibili effettivamente.

Il passaggio Muller -> parity sembra complicare l'arena, perche' aggiunge la memoria LAR. Pero' semplifica la winning condition e permette di usare la teoria dei parity games.

La memoria non sparisce: viene spostata nello stato del gioco simulato.

53. Determinazione dei parity games

Il teorema dice:

ogni parity game finito e' determinato, e le winning regions sono calcolabili.

In piu':

il giocatore vincente ha una strategia posizionale.

Questa frase e' importante:

• nel parity game simulato basta guardare lo stato corrente;
• ma lo stato corrente include anche il LAR;
• quindi nel gioco Muller originale la strategia corrispondente e' a memoria finita.

54. Complessita dei parity games

Il problema:

dato un parity game e uno stato $q$, decidere se $q\in W_B$

e' noto essere in:

$$NP\cap coNP.$$

Il fatto che sia in $NP\cap coNP$ suggerisce che non e' probabilmente NP-completo, ma non implica automaticamente un algoritmo polinomiale. La complessita' dei parity games e' un tema importante della teoria algoritmica dei giochi.

Per il corso basta ricordare:

• la soluzione e' effettiva;
• le strategie posizionali esistono;
• la complessita' e' delicata;
• i parity games sono centrali anche nel mu-calcolo.

Parte IX - Soluzione di Church's Problem

55. Teorema di Buchi-Landweber

Il teorema di Buchi-Landweber dice:

per specifiche S1S, Church's problem e' decidibile; se una soluzione esiste, e' possibile costruire una macchina a stati finiti che la realizza.

Detto in modo operativo:

1. ricevi una formula S1S $\varphi(X,Y)$;
2. decidi se e' realizzabile;
3. se e' realizzabile, costruisci un automa di Mealy.

Questo e' molto piu' forte di una semplice procedura decisionale yes/no.

56. Pipeline completa

La pipeline e':

$$ \varphi(X,Y) \to \mathcal{A}_\varphi \to G_\varphi \to \text{parity game} \to \text{strategia vincente} \to \text{Mealy}. $$

Con parole:

1. S1S -> automa deterministico di Muller sulle coppie input/output.
2. Automa -> gioco di Muller, separando input e output.
3. Gioco di Muller -> gioco di parita tramite LAR.
4. Risoluzione del parity game.
5. Se lo stato iniziale e' vincente per B, costruzione della strategia.
6. Strategia -> automa di Mealy finale.

57. Dove entra esattamente Buchi-Landweber

Il teorema entra nel punto in cui bisogna sapere che:

• i giochi di Muller sono determinati;
• le winning regions sono calcolabili;
• se il sistema vince, esiste una strategia a memoria finita costruibile.

Senza questo risultato avremmo:

• una specifica;
• un automa;
• un gioco;

ma non avremmo la garanzia che il gioco porti a una macchina finita.

Buchi-Landweber chiude proprio questo buco.

58. Come si costruisce il Mealy finale

Supponi di avere:

• l'automa di Muller della specifica, con stati $Q$;
• un automa di strategia, con memoria $S$.

Il Mealy finale usa stati del tipo:

$$Q\times S.$$

Un suo stato:

$$(q,s)$$

significa:

• $q$ = dove si trova l'automa della specifica;
• $s$ = qual e' la memoria attuale della strategia.

Quando arriva un input $b$:

1. il gioco entra nello stato intermedio $(q,b)$;
2. la strategia aggiorna la memoria;
3. la strategia sceglie un'uscita del gioco;
4. da questa uscita si ricava l'output $c$;
5. l'automa di Muller avanza a $q'=\delta(q,(b,c))$;
6. la memoria diventa $s'$.

Il nuovo stato del Mealy e':

$$(q',s').$$

Questa e' la ragione tecnica per cui il Mealy finale combina automa della specifica e automa della strategia.

59. Caso vincente e caso perdente

Dopo aver risolto il gioco, guardiamo lo stato iniziale.

Se:

$$q_0\in W_B,$$

allora il sistema ha una strategia vincente. La specifica e' realizzabile e possiamo costruire il Mealy.

Se:

$$q_0\in W_A,$$

allora l'ambiente ha una strategia vincente. La specifica non e' realizzabile: qualunque controllore il sistema scelga, l'ambiente puo' produrre input che violano la specifica.

Questa risposta negativa e' importante: non significa che l'algoritmo non ha trovato il controllore. Significa che il controllore non esiste.

60. Esempio: vincoli su input e output binari

Negli appunti compare un esempio con input $\alpha$ e output $\beta$ binari. Vincoli tipici:

1. se l'input e' 1, allora l'output deve essere 1;
2. non possono comparire due 0 consecutivi nell'output;
3. se l'input contiene infiniti 0, allora anche l'output deve contenere infiniti 0.

Il primo vincolo da solo ammette la soluzione banale:

produci sempre 1.

Il terzo vincolo elimina questa soluzione, perche' se l'input ha infiniti 0, anche l'output deve avere infiniti 0.

Il secondo vincolo impedisce di copiare ciecamente l'input, perche' l'ambiente potrebbe produrre due 0 consecutivi.

La soluzione, se esiste, deve usare memoria finita per decidere quando emettere 0 senza crearne due consecutivi, ma garantendo infiniti 0 quando l'ambiente li offre infinitamente spesso.

Il punto dell'esempio e':

il sistema non sceglie una singola sequenza $\beta$; sceglie una regola finita per produrre $\beta$ contro ogni input $\alpha$.

61. Sintesi LTL e varianti

Gli appunti chiudono osservando che Church's problem ha molte varianti.

Si puo' cambiare:

• il linguaggio di specifica;
• la struttura input/output;
• il tipo di memoria consentita;
• la winning condition;
• il modello temporale.

La sintesi LTL moderna e' una prosecuzione naturale:

una specifica temporale descrive il comportamento desiderato, e il problema e' costruire un controllore che la realizza contro l'ambiente.

Il capitolo 10 non chiede di conoscere tutta la teoria moderna della sintesi LTL. Chiede di capire il risultato classico:

logica -> automi -> giochi -> strategie -> controllori.

Parte X - Quadro finale

62. Confronto con il capitolo 9

Il capitolo 9 e il capitolo 10 sono collegati, ma rispondono a domande diverse.

Nel capitolo 9 il sistema e' gia' fissato.

Nel capitolo 10 il sistema deve essere costruito.

63. La frase chiave del capitolo

La frase da ricordare e':

la sintesi e' una verifica contro un ambiente avversario, dove il risultato positivo non e' solo "vero", ma una strategia implementabile.

Se sai spiegare questa frase, hai gia' il nucleo del capitolo.

64. Errori tipici

Confondere sintesi e model building

Model building puo' significare: data una formula soddisfacibile, costruisci un modello.

La sintesi qui e': costruisci un controllore che funziona per ogni input dell'ambiente.

Pensare che basti $\exists Y$

Non basta trovare un output buono. Serve una funzione online e finite-state che produca output per ogni input.

Dimenticare il vincolo online

Specifiche come:

$$\beta(t)=\alpha(t+1)$$

possono sembrare semplici, ma non sono realizzabili online.

Confondere automa della specifica e controllore

L'automa di Muller riconosce coppie input/output corrette. Il controllore Mealy produce output. Sono oggetti diversi.

Confondere stati del gioco e stati del Mealy

Il gioco e' l'arena. Il Mealy implementa una strategia. Il Mealy finale puo' avere stati del tipo $Q\times S$, non semplicemente gli stati dell'arena.

Pensare che Muller e weak Muller siano uguali

Weak Muller guarda $Occ(\rho)$, cioe' gli stati visitati almeno una volta. Muller guarda $Inf(\rho)$, cioe' gli stati visitati infinitamente spesso.

Pensare che LAR sia solo una lista

La lista da sola non basta. Servono anche hit e hitting set, per collegare le ultime apparizioni all'insieme $Inf(\rho)$.

Pensare che i parity games richiedano memoria

I parity games ammettono strategie posizionali. La memoria sta nella simulazione LAR: lo stato del gioco simulato include cio' che nel gioco Muller era memoria.

65. Mini-esercizi guidati

Esercizio 1: online

Specifica:

$$\beta(t)=\alpha(t+1).$$

E' realizzabile online?

No. Per produrre $\beta(t)$ bisogna conoscere l'input futuro $\alpha(t+1)$.

Esercizio 2: finite-state

Specifica:

l'output al tempo $t$ e' il numero esatto di 1 comparsi finora.

E' realizzabile con un Mealy finito?

No, se il numero deve essere esatto e illimitato. Serve memoria non limitata.

Esercizio 3: soddisfacibilita' contro sintesi

Supponi che esista una coppia $(\alpha,\beta)$ che soddisfa $\varphi$.

Questo implica che la specifica sia sintetizzabile?

No. Significa solo:

$$\exists X\exists Y.\ \varphi(X,Y).$$

La sintesi richiede una strategia per ogni input.

Esercizio 4: attractor

Se $q\in Q_B$ ha almeno un successore in $Attr_B(F)$, perche' entra nell'attrattore?

Perche' in $q$ sceglie B, quindi puo' scegliere quel successore.

Se $q\in Q_A$, perche' servono tutti i successori nell'attrattore?

Perche' in $q$ sceglie A, e B deve vincere contro ogni scelta dell'ambiente.

Esercizio 5: weak Muller vs Muller

Per:

$$\rho=a,b,c,b,c,b,c,\ldots$$

calcola $Occ(\rho)$ e $Inf(\rho)$.

Soluzione:

$$Occ(\rho)=\{a,b,c\},$$

$$Inf(\rho)=\{b,c\}.$$

Esercizio 6: LAR

Se il LAR e':

$$((D,C,B,A),2),$$

qual e' l'hitting set?

Soluzione:

$$H=\{D,C\}.$$

Esercizio 7: colore LAR

Sia:

$$\mathcal{F}=\{\{D,C\}\}.$$

Per il LAR:

$$((D,C,B,A),2),$$

il colore e' pari o dispari?

Poiche':

$$H=\{D,C\}\in\mathcal{F},$$

il colore e':

$$2h=4,$$

quindi pari.

Esercizio 8: Mealy finale

Perche' il Mealy finale usa stati $Q\times S$?

Perche' deve sapere sia:

• lo stato dell'automa della specifica;
• la memoria della strategia vincente.

66. Mappa per l'orale

Per rispondere bene:

1. Parti dalla differenza fra model checking e sintesi.
2. Spiega che il sistema controlla output, non input.
3. Definisci Church's problem: sequenza input $\alpha$, sequenza output $\beta$, specifica S1S $\varphi(X,Y)$.
4. Spiega online e finite-state.
5. Definisci automa di Mealy.
6. Spiega perche $\exists X\exists Y$ non basta.
7. Dai la pipeline Buchi-Landweber.
8. Spiega S1S -> automa deterministico di Muller.
9. Spiega perche Muller: determinismo ed espressivita' omega-regolare.
10. Spiega automa -> gioco separando input e output.
11. Definisci arena, play, winning condition.
12. Definisci strategia vincente e winning region.
13. Distingui reachability, weak Muller e Muller.
14. Spiega attractor per reachability.
15. Spiega perche weak Muller puo' richiedere memoria.
16. Spiega LAR: lista, hit, hitting set.
17. Spiega Muller -> parity tramite colori.
18. Spiega perche i parity games sono utili: determinazione e strategie posizionali.
19. Chiudi con la costruzione del Mealy finale.

67. Risposta orale pronta

Una risposta compatta:

La sintesi automatica cerca di costruire un sistema finito a partire da una specifica, mentre il model checking verifica un sistema gia' dato. Nel problema di Church l'ambiente produce una sequenza infinita di input e il sistema deve produrre online una sequenza infinita di output, in modo che la coppia input/output soddisfi una specifica S1S. La soluzione cercata e' un automa di Mealy, quindi una strategia a memoria finita.

Il teorema di Buchi-Landweber mostra che, per S1S, il problema e' decidibile: si trasforma la formula in un automa deterministico di Muller sulle coppie input/output, poi l'automa in un gioco di Muller che separa le mosse dell'ambiente e del sistema. Risolvere il gioco significa stabilire se il sistema ha una strategia vincente. I giochi di Muller vengono gestiti trasformandoli in giochi di parita tramite LAR, che registra l'ordine delle ultime apparizioni, l'hit e l'hitting set. Se lo stato iniziale e' vincente per il sistema, la strategia risultante viene implementata come automa di Mealy.

68. Riassunto finale

Il capitolo 10 combina logica, automi e giochi.

La logica S1S esprime la specifica. Gli automi riconoscono le coppie input/output che soddisfano la specifica. I giochi separano il ruolo dell'ambiente e del sistema. Le strategie vincenti rappresentano controllori. Gli automi di Mealy implementano queste strategie.

La catena da ricordare e':

$$ \text{S1S} \to \text{Muller automaton} \to \text{Muller game} \to \text{parity game tramite LAR} \to \text{winning strategy} \to \text{Mealy controller}. $$

La sintesi e' quindi model checking rovesciato e rafforzato:

non chiedo se un modello dato e' corretto; chiedo se esiste una strategia finita che rende vera la specifica contro ogni comportamento dell'ambiente.