Pianificazione come model checking

Il planning come model checking rappresenta un dominio di pianificazione come sistema di transizione e il goal come proprieta' da raggiungere o verificare.

La differenza rispetto al model checking classico e' che qui non ci limitiamo a controllare un modello gia' fissato: cerchiamo una state-action table, cioe' un piano, che induca una execution structure con la proprieta' richiesta.

Dominio

Un dominio non deterministico puo' essere descritto come:

$$D=(P,S,A,R).$$

Dove:

• $P$ e' un insieme finito di proposizioni, spesso del tipo fluent = value;
• $S\subseteq 2^P$ e' l'insieme degli stati validi;
• $A$ e' l'insieme finito delle azioni;
• $R\subseteq S\times A\times S$ e' la relazione di transizione.

Un'azione $a$ e' abilitata in uno stato $s$ se esiste almeno un successore $s'$ tale che $(s,a,s')\in R$.

Fluents

I fluents descrivono il dominio.

• Inerziali: cambiano solo per effetto di azioni del piano.
• Non inerziali: possono cambiare indipendentemente dal piano, per effetto dell'ambiente.

Questa distinzione spiega molte sorgenti di non determinismo: il piano controlla le azioni, ma non sempre controlla l'ambiente.

Piani

Un piano e' rappresentabile come:

$$SA\subseteq S\times A.$$

Ogni coppia $(s,a)$ dice che nello stato $s$ l'azione $a$ e' ammessa dal piano.

Una state-action table puo' essere:

• deterministica, se per ogni stato contiene al piu' un'azione;
• non deterministica, se per uno stato contiene piu' azioni;
• universale, se associa almeno un'azione a ogni stato del dominio.

Execution Structure

Data una state-action table $SA$ e un insieme di iniziali $I$, si costruisce la execution structure:

$$K=(Q,T).$$

$Q$ contiene gli stati raggiungibili da $I$ eseguendo azioni ammesse da $SA$. $T$ contiene le transizioni indotte da $SA$ e dalla relazione $R$.

Uno stato terminale e' uno stato senza successori in $T$.

Soluzioni

• Weak solution: da ogni stato iniziale esiste almeno un cammino della execution structure che raggiunge un goal. E' una garanzia esistenziale.
• Strong solution: la execution structure e' aciclica e tutti i terminali sono goal. Quindi tutti i cammini terminano correttamente.
• Strong-cyclic solution: da ogni stato raggiungibile resta possibile arrivare al goal, e tutti i terminali sono goal. Ammette cicli, ma garantisce il goal sotto ipotesi di fairness.

La relazione di inclusione e':

$$\text{strong}\subseteq \text{strong-cyclic}\subseteq \text{weak}.$$

Determinizzazioni

Se $SA$ e' non deterministica, una determinizzazione $SA'\subseteq SA$ sceglie una sola azione per ogni stato coperto da $SA$.

Una state-action table non deterministica e' weak, strong o strong-cyclic se tutte le sue determinizzazioni hanno la proprieta' corrispondente.

Tecnica simbolica

Weak e strong preimage permettono di calcolare piani come insiemi di coppie stato-azione rappresentati simbolicamente.

• La weak preimage usa una condizione esistenziale sui successori: esiste un'azione con almeno un successore nella regione target.
• La strong preimage usa una condizione universale sui successori: esiste un'azione applicabile i cui successori sono tutti nella regione target.

La condizione di applicabilita' e' necessaria per evitare che un'azione non abilitata soddisfi vacuamente la quantificazione universale.

Collegamenti

• Linguaggio di descrizione delle azioni AR
• Model checking simbolico
• CTL

Linguaggio di descrizione delle azioni AR

Il linguaggio $\mathcal{AR}$ e' un linguaggio di descrizione di azioni usato per modellare problemi di pianificazione in domini non deterministici.

Serve a descrivere:

• effetti obbligatori delle azioni;
• effetti possibili e quindi non deterministici;
• vincoli validi in tutti gli stati;
• stati iniziali;
• stati goal.

Una descrizione $\mathcal{AR}$ puo' essere compilata in una relazione di transizione simbolica:

$$R(\vec{x},\vec{a},\vec{x}').$$

Regole principali

A CAUSES P IF Q

Significa:

se l'azione $A$ viene eseguita in uno stato in cui vale $Q$, allora nel successore deve valere $P$.

Schema:

$$A(\vec{a})\land Q(\vec{x})\Rightarrow P(\vec{x}').$$

A POSSIBLY CHANGES F IF Q

Significa:

se $A$ viene eseguita in una situazione in cui vale $Q$, allora il fluent $F$ puo' cambiare valore.

Questa regola introduce non determinismo: il cambiamento e' permesso, non imposto.

ALWAYS P

Impone un vincolo di integrita' su tutti gli stati validi.

Esempio: se la posizione puo' essere solo station, traffic light o airport, si usano vincoli ALWAYS per impedire che due posizioni siano vere insieme.

INITIALLY P

Descrive gli stati iniziali.

Se INITIALLY station non specifica il colore del semaforo, allora entrambi gli stati station/red e station/green possono essere iniziali.

GOAL G

Descrive gli stati goal.

Se GOAL airport non specifica il colore del semaforo, allora sia airport/red sia airport/green sono goal.

Inerzia

I fluents inerziali non devono cambiare senza motivo. Cambiano solo se:

• un'azione li causa;
• una regola POSSIBLY CHANGES ne permette il cambiamento.

Questo evita transizioni spurie, ad esempio un pacco che cambia posizione senza azione di trasporto.

Esempio tipico

Nel dominio pacco-semaforo:

transportation CAUSES traffic_light IF station
transportation CAUSES airport IF traffic_light and light = green
transportation CAUSES false IF not (station or (traffic_light and light = green))
wait CAUSES false IF not traffic_light
ALWAYS station <-> not (traffic_light or airport)
ALWAYS traffic_light <-> not (station or airport)
ALWAYS airport <-> not (traffic_light or station)
INITIALLY station
GOAL airport

Le regole CAUSES false codificano azioni non applicabili. I vincoli ALWAYS codificano la consistenza degli stati.

Uso in V&V

Le descrizioni in $\mathcal{AR}$ permettono di passare da una descrizione dichiarativa del dominio a formule booleane usate nel model checking simbolico.

In questo modo un problema di planning diventa manipolabile con:

• insiemi simbolici di stati;
• preimmagini weak e strong;
• calcolo di state-action tables;
• verifica di soluzioni weak, strong e strong-cyclic.

Collegamenti

• Pianificazione come model checking
• Model checking simbolico
• Model checking
• Panoramica degli appunti

Approfondimento completo settimana 6 - Planning non deterministico via Symbolic Model Checking

Questo capitolo chiude il percorso del corso: dopo model checking, logiche temporali, automi, sintesi e giochi, si arriva al planning non deterministico.

L'idea centrale e':

un problema di pianificazione puo' essere visto come un problema di model checking e, piu' precisamente, come un problema di costruzione/verifica di un piano su un sistema di transizione.

La parola chiave e' piano. Un piano non e' sempre una lista fissa di azioni. In domini non deterministici deve spesso essere una tabella, una strategia o un controllore che sceglie cosa fare in base allo stato osservato.

Questo e' il collegamento con il capitolo 10: li' abbiamo sintetizzato un controller reattivo; qui sintetizziamo o verifichiamo un controller di planning.

1. Perche' il planning entra in V&V

Nel model checking classico la domanda e':

dato un modello $M$ e una proprieta' $\varphi$, tutte le computazioni rilevanti di $M$ soddisfano $\varphi$?

Nel planning la domanda e':

dato un dominio, un insieme di stati iniziali, un goal e un insieme di azioni, esiste un modo di scegliere azioni che porta al goal?

Quindi non stiamo solo verificando un sistema gia' fissato. Stiamo cercando una politica di comportamento.

La differenza e' questa:

• nel model checking, il comportamento del sistema e' gia' dato;
• nel planning, una parte del comportamento deve essere scelta dal piano;
• nel planning non deterministico, dopo una scelta del piano possono comunque esserci esiti non controllati.

Questa ultima parte e' fondamentale. Se un'azione puo' avere piu' effetti, il piano non controlla tutto. Deve essere robusto rispetto all'incertezza ammessa dal dominio.

2. Action-based planning e timeline-based planning

Gli appunti distinguono:

• action-based planning;
• timeline-based planning.

Nel capitolo si lavora con l'action-based planning.

Action-based significa che il piano e' costruito a partire da:

• azioni disponibili;
• precondizioni delle azioni;
• effetti delle azioni;
• stati iniziali;
• stati goal.

Il problema e' quindi:

trovare azioni, o una regola per scegliere azioni, che trasformino uno stato iniziale in uno stato goal.

Timeline-based planning invece ragiona piu' esplicitamente su variabili che evolvono lungo linee temporali, durate, vincoli temporali e assegnamenti nel tempo. Negli appunti e' citato come confronto, ma la formalizzazione sviluppata qui e' quella action-based.

3. Questioni principali nel planning automatico

Gli appunti elencano alcune questioni generali:

• espressivita';
• decidibilita' e complessita';
• planning as satisfiability checking;
• planning as model checking;
• sintesi di plan controllers;
• monitoring dell'esecuzione del piano.

Non sono punti decorativi: spiegano perche' il planning e' difficile.

Espressivita' (expressiveness)

Un formalismo di planning deve descrivere:

• stati;
• azioni;
• precondizioni;
• effetti;
• incertezza;
• vincoli durante l'esecuzione;
• goal finali.

Un formalismo piu' espressivo permette di descrivere domini piu' realistici, ma spesso rende piu' difficile decidere se esiste un piano.

Decidibilita' (decidability) e complessita'

Nel caso studiato qui il dominio e' finito: fluents finiti, stati finiti, azioni finite. In questo caso i problemi principali sono decidibili.

Ma la decidibilita' non e' automatica in ogni variante. Se si passa, per esempio, a domini temporali densi come il tempo reale continuo, alcune versioni del planning diventano indecidibili.

Quindi il corso lavora in un setting finito e simbolico: abbastanza ricco per modellare domini non deterministici, ma abbastanza controllato da permettere algoritmi.

Planning as satisfiability checking

Un modo classico di affrontare il planning e' codificare:

• stati al tempo $0,1,\ldots,k$;
• azioni scelte nei vari passi;
• transizioni;
• goal al tempo $k$;

come una formula SAT.

Se la formula e' soddisfacibile, l'assegnamento trovato descrive un piano di lunghezza $k$.

Questa idea e' vicina al bounded model checking del capitolo 9: si fissa un bound e si cerca una testimonianza finita.

Planning as model checking

Nel planning come model checking il dominio diventa un modello, e il goal diventa una proprieta' di raggiungibilita' o una formula temporale.

Il vantaggio e' che si possono riusare:

• rappresentazioni simboliche;
• preimmagini;
• punti fissi;
• ragionamento su tutti i cammini o su qualche cammino.

Plan controllers

Non basta sapere che un piano esiste. Bisogna anche eseguirlo.

Per questo gli appunti parlano di synthesis of plan controllers. Il risultato desiderato non e' solo "si/no", ma un oggetto operativo:

• una state-action table;
• una politica;
• un controller che osserva lo stato e sceglie un'azione.

Monitoring

Nei domini realistici il piano viene eseguito dentro un ambiente non totalmente controllato.

Quindi durante l'esecuzione bisogna misurare parametri ambientali e adattare la scelta dell'azione. Questo e' il motivo per cui i piani situated e universal sono importanti.

4. Il planning problem in forma intuitiva

La definizione intuitiva e':

trovare una sequenza di azioni che porta un sistema da uno stato iniziale a uno stato goal.

Questa e' la versione piu' semplice. Ma nel planning non deterministico la sequenza fissa spesso non basta, perche':

• potrei non conoscere esattamente lo stato iniziale;
• l'ambiente potrebbe cambiare variabili non controllate;
• un'azione potrebbe avere effetti diversi;
• potrei dover controllare vincoli durante l'esecuzione, non solo il goal finale.

Per questo il piano viene rappresentato come relazione stato-azione, non solo come lista:

$$SA\subseteq S\times A.$$

Il piano dice:

se sei nello stato $s$, puoi/esegui l'azione $a$.

5. Elementi del problema

Un problema di planning contiene:

• un dominio o contesto;
• un insieme di stati iniziali;
• un insieme di stati goal;
• un insieme di azioni;
• una relazione che descrive gli effetti delle azioni.

Nel dominio compaiono variabili, chiamate spesso fluents, che descrivono il mondo.

Esempi di fluent:

• posizione del pacco;
• colore del semaforo;
• porta aperta/chiusa;
• batteria alta/bassa;
• robot in stanza A/B/C.

Uno stato e' una configurazione completa dei fluents.

6. Fluents inerziali e non inerziali

Gli appunti distinguono due tipi di fluents.

Fluents inerziali

Un fluent e' inerziale se il suo valore cambia solo come effetto di un'azione del piano.

Esempio:

• la posizione del pacco cambia se eseguo transport;
• la posizione del robot cambia se eseguo move;
• una porta cambia da chiusa ad aperta se eseguo open.

Il punto e':

un fluent inerziale non cambia spontaneamente.

Questa e' una forma di frame assumption: cio' che non viene modificato da un'azione resta uguale.

Fluents non inerziali

Un fluent e' non inerziale se puo' cambiare indipendentemente dalle azioni del piano.

Esempio:

• colore del semaforo;
• meteo;
• disponibilita' di una risorsa esterna;
• stato di un sensore controllato dall'ambiente.

Il punto e':

il piano non controlla direttamente quel valore.

Questa distinzione e' una delle radici del non determinismo.

7. Il caso semplice standard

Il corso parte da un setting ristretto:

• domini finiti o discreti;
• tempo discreto;
• osservabilita' completa;
• assenza di eventi esterni;
• azioni deterministiche.

In questo caso il planning e' piu' vicino alla ricerca in un grafo:

1. parti da uno stato iniziale;
2. scegli un'azione;
3. arrivi a un successore unico;
4. ripeti finche' raggiungi il goal.

Queste ipotesi sono utili per capire la base, ma vengono rilassate appena si entra nel planning non deterministico.

8. Dove nasce il non determinismo (nondeterminism)

Gli appunti indicano tre sorgenti principali di non determinismo.

Eventi esterni

L'ambiente puo' cambiare alcune variabili indipendentemente dal piano.

Esempio: il semaforo puo' diventare rosso o verde.

Specifica parziale degli stati iniziali

Potrei sapere che il pacco e' alla stazione, ma non sapere se il semaforo e' rosso o verde.

Allora non ho un singolo stato iniziale, ma un insieme:

$$I\subseteq S.$$

Il piano deve funzionare rispetto agli stati iniziali ammessi.

Incertezza sugli effetti delle azioni

Una stessa azione puo' produrre piu' successori.

Formalmente:

$$R\subseteq S\times A\times S.$$

Se per una coppia $(s,a)$ esistono piu' $s'$ tali che $(s,a,s')\in R$, allora l'azione e' non deterministica.

9. Extended goals

Nel planning piu' semplice il goal e' solo:

raggiungi uno stato finale desiderato.

Ma spesso non basta. Potrei volere anche:

• non passare mai per stati pericolosi;
• mantenere vincoli di integrita';
• evitare deadlock;
• visitare certi stati prima di altri;
• garantire una proprieta' temporale durante l'esecuzione.

Questi sono extended goals.

Qui entra la logica temporale:

• safety: "non accade mai qualcosa di cattivo";
• reachability: "prima o poi raggiungo il goal";
• response: "se accade una richiesta, prima o poi rispondo";
• fairness o recurrence: "certe condizioni favorevoli non vengono ignorate per sempre".

Nel capitolo 11 il focus resta soprattutto sulla reachability, ma gli appunti motivano perche' una formula temporale puo' descrivere goal piu' ricchi.

10. Situated, universal e conformant plans

Gli appunti classificano i piani in tre famiglie.

Situated plans

Un situated plan osserva l'ambiente durante l'esecuzione.

L'idea e':

misuro lo stato o il contesto corrente, poi scelgo l'azione.

Questo tipo di piano e' adatto a domini in cui:

• ci sono fluents non inerziali;
• l'ambiente puo' evolvere;
• la scelta migliore dipende dalla misura corrente;
• il piano puo' usare trial and error.

Esempio: se sono al semaforo e vedo rosso, aspetto; se vedo verde, trasporto.

Universal plans

Un universal plan associa almeno un'azione a ogni stato possibile del dominio.

Formalmente, per ogni $s\in S$ esiste almeno un $a\in A$ tale che:

$$(s,a)\in SA.$$

E' un caso speciale di situated plan: qualunque sia lo stato osservato, il piano sa cosa proporre.

Attenzione: un piano universale non esiste sempre. Alcuni stati potrebbero essere irrimediabilmente perdenti, oppure non avere azioni utili.

Conformant plans

Un conformant plan non richiede osservazioni durante l'esecuzione.

Serve quando:

• non posso misurare l'ambiente;
• non ho osservabilita';
• devo garantire il goal qualunque sia l'evoluzione ammessa.

Questo e' piu' difficile. Se non posso osservare, non posso adattare il piano a cio' che succede.

11. Planning as model checking

Il collegamento con il model checking e':

• il dominio di planning diventa il modello;
• il goal diventa la formula;
• il piano diventa una restrizione/scelta delle transizioni.

Nel model checking classico:

$$M\models \varphi.$$

Nel planning:

cerco una state-action table $SA$ tale che la execution structure indotta da $SA$ soddisfi la proprieta' richiesta.

Quindi non verifico solo il dominio completo. Verifico il sottosistema generato dal piano.

12. Dominio di planning non deterministico

La definizione degli appunti e':

$$D=(P,S,A,R).$$

Dove:

• $P$ e' un insieme finito di lettere proposizionali;
• $S\subseteq 2^P$ e' un insieme finito di stati;
• $A$ e' un insieme finito di azioni;
• $R\subseteq S\times A\times S$ e' la relazione di transizione.

Le lettere proposizionali hanno spesso la forma:

$$fluent_i=value_j.$$

Esempio:

• position = station;
• position = traffic_light;
• light = red;
• light = green.

Uno stato e' l'insieme delle lettere vere in quella configurazione.

13. Perche' $S\subseteq 2^P$

Se $P$ contiene tutte le proposizioni atomiche, allora ogni stato puo' essere identificato con il sottoinsieme di $P$ vero in quello stato.

Esempio:

$$s=\{position=station,\ light=red\}.$$

Questo significa:

• la posizione e' station;
• il semaforo e' red;
• le altre proposizioni incompatibili sono false.

La notazione $S\subseteq 2^P$ ricorda che non ogni sottoinsieme di $P$ e' necessariamente uno stato valido.

Per esempio non voglio uno stato in cui siano vere insieme:

• position = station;
• position = airport.

I vincoli di consistenza eliminano valutazioni impossibili.

14. Azioni abilitate

Un'azione $a$ e' enabled in uno stato $s$ se esiste almeno un successore $s'$ tale che:

$$(s,a,s')\in R.$$

Quindi:

$$enabled(s,a)\quad\text{se e solo se}\quad \exists s'.\ R(s,a,s').$$

Questo e' il modo formale per dire che un'azione e' applicabile.

Se transport non puo' essere eseguita con il semaforo rosso, allora in quello stato non ci sara' nessuna transizione valida associata a transport.

15. Deterministico vs non deterministico

Nel caso deterministico, per ogni stato e azione abilitata esiste al piu' un successore:

$$(s,a)\mapsto s'.$$

Nel caso non deterministico, possono esistere piu' successori:

$$(s,a)\mapsto \{s'_1,s'_2,\ldots\}.$$

La relazione $R$ e' quindi piu' generale di una funzione.

Questa differenza e' il motivo per cui weak, strong e strong-cyclic non coincidono.

16. Esempio del pacco e del semaforo

L'esempio degli appunti:

un pacco deve essere trasferito dalla stazione ferroviaria all'aeroporto.

Sul percorso c'e' un semaforo. Il veicolo puo' dover aspettare il verde.

I fluents principali sono:

• position, inerziale;
• light, non inerziale.

Valori possibili:

• position in {station, traffic_light, airport};
• light in {red, green}.

Stati iniziali:

• pacco alla stazione;
• colore del semaforo non necessariamente noto.

Quindi potrei avere:

$$I=\{(station,red),(station,green)\}.$$

Stati goal:

• pacco all'aeroporto;
• il colore del semaforo non importa piu'.

Quindi:

$$G=\{(airport,red),(airport,green)\}.$$

17. Perche' il colore del semaforo causa esplosione di stati

Il goal riguarda la posizione del pacco, ma lo stato formale include anche il colore del semaforo.

Quindi devo distinguere:

• station/red;
• station/green;
• traffic_light/red;
• traffic_light/green;
• airport/red;
• airport/green.

Anche se in aeroporto il colore e' irrilevante per il goal, il modello simbolico lo rappresenta comunque.

Questo e' un piccolo esempio dello state explosion problem:

variabili indipendenti o quasi indipendenti producono un prodotto cartesiano di configurazioni.

Il symbolic model checking aiuta perche' rappresenta insiemi di stati con formule booleane, invece di enumerare ogni stato uno per uno.

18. Azioni nell'esempio

Le azioni principali sono:

• transport;
• wait.

transport sposta il pacco:

• da station a traffic_light;
• da traffic_light a airport, ma solo se light=green.

wait serve quando si e' al semaforo.

Il colore del semaforo puo' cambiare in modo non controllato:

• da red a green;
• da green a red;
• o restare uguale, a seconda della modellazione.

La precondizione importante e':

non posso trasportare dal semaforo all'aeroporto se il semaforo e' rosso.

19. Piano come state-action table

Un piano puo' essere rappresentato da una state-action table:

$$SA\subseteq S\times A.$$

Ogni coppia $(s,a)$ dice:

nello stato $s$, il piano ammette l'azione $a$.

La condizione minima e' che $a$ sia enabled in $s$.

Quindi una tabella non dovrebbe contenere coppie impossibili, come:

$$(traffic\_light,red,\ transport)$$

se il trasporto con rosso non e' abilitato.

20. Piani deterministici e universali

Un piano e' deterministico se per ogni stato c'e' al piu' una coppia:

$$|\{a\mid (s,a)\in SA\}|\le 1.$$

Un piano e' universale se per ogni stato c'e' almeno una coppia:

$$|\{a\mid (s,a)\in SA\}|\ge 1.$$

Queste due proprieta' sono diverse:

• deterministico: non lascia scelta tra piu' azioni;
• universale: copre tutti gli stati.

Un piano puo' essere:

• deterministico ma non universale;
• universale ma non deterministico;
• entrambe le cose;
• nessuna delle due.

21. Piani non deterministici

Una state-action table e' non deterministica se in uno stesso stato ammette piu' azioni:

$$(s,a_1)\in SA,\quad (s,a_2)\in SA,\quad a_1\ne a_2.$$

Questo non va confuso con il non determinismo della transizione.

Ci sono due livelli:

1. il piano puo' ammettere piu' azioni nello stesso stato;
2. il dominio puo' far evolvere una stessa azione verso piu' successori.

Il primo e' non determinismo nella scelta del piano. Il secondo e' non determinismo dell'ambiente o dell'azione.

22. Rappresentazione alternativa: ACT e CTXT

Gli appunti citano anche una rappresentazione alternativa che distingue:

• stato dell'agente/sistema;
• contesto.

Usa funzioni del tipo:

$$ACT(q,c)$$

che specifica l'azione da eseguire quando il sistema e' nello stato $q$ e nel contesto $c$.

E:

$$CTXT(q,c,q')$$

che aggiorna il contesto dopo aver raggiunto $q'$.

Questa rappresentazione non viene sviluppata nel corso, ma serve a far capire che un piano puo' essere visto come un controller contestuale.

23. Execution structure

Data una state-action table $SA$, si costruisce la execution structure.

Intuizione:

e' il grafo di tutte le esecuzioni possibili del piano.

Il dominio contiene tutte le transizioni possibili. La state-action table sceglie quali azioni sono ammesse. La execution structure tiene solo le transizioni indotte da quelle azioni, partendo dagli stati iniziali.

Formalmente, data:

$$D=(P,S,A,R),$$

una state-action table $SA$ e un insieme di iniziali $I$, la execution structure e':

$$K=(Q,T).$$

Dove $Q\subseteq S$ e $T\subseteq S\times S$ sono i minimi insiemi tali che:

1. se $s\in I$, allora $s\in Q$;
2. se $s\in Q$, $(s,a)\in SA$ e $R(s,a,s')$, allora $s'\in Q$ e $(s,s')\in T$.

La parola "minimi" significa che $Q$ contiene solo gli stati raggiungibili eseguendo il piano, non tutti gli stati del dominio.

24. Perche' la execution structure e' una Kripke structure

La execution structure e' sostanzialmente una struttura di Kripke:

• nodi = stati raggiungibili;
• archi = transizioni possibili indotte dal piano;
• etichette = proposizioni vere negli stati.

La differenza rispetto ad alcune definizioni classiche di Kripke e' che qui il grafo non deve per forza essere totale.

Puo' contenere stati terminali.

Questo e' naturale nel planning, perche' un piano puo' terminare quando arriva al goal.

25. Stati terminali

Uno stato $s\in Q$ e' terminale se non esiste nessuno stato $s'$ tale che:

$$(s,s')\in T.$$

In parole:

l'esecuzione si ferma.

Uno stato terminale non e' per forza buono. E' buono se e' un goal.

Un piano che si blocca in uno stato non-goal e' difettoso per strong planning.

26. Execution paths

Un execution path da $s_0\in I$ e' una sequenza:

$$s_0,s_1,s_2,\ldots$$

tale che per ogni $i$:

• o $s_i$ e' l'ultimo stato della sequenza, quindi terminale;
• oppure $(s_i,s_{i+1})\in T$.

Il path puo' essere:

• finito, se termina;
• infinito, se continua per sempre.

Nel planning di reachability, i path infiniti sono pericolosi quando evitano per sempre il goal.

27. Raggiungibilita' e aciclicita'

Uno stato $s'$ e' raggiungibile da $s$ se esiste un path da $s$ a $s'$.

La execution structure $K$ e' aciclica se tutti i suoi execution paths sono finiti.

Attenzione: "aciclica" qui e' legata al fatto che non si puo' restare in un ciclo infinito. Se non ci sono cicli raggiungibili, ogni path prima o poi termina.

Questa nozione e' cruciale per strong solutions.

28. Esempio di piano sbagliato nel semaforo

Supponiamo di costruire un piano che dice:

• se sei alla stazione, fai transport;
• se sei al semaforo e il semaforo e' verde, fai transport;
• non includere wait quando il semaforo e' rosso.

Questo piano puo' sembrare ragionevole, perche' trasporta appena possibile.

Ma se arrivi a:

$$traffic\_light/red$$

e non hai l'azione wait, sei bloccato in uno stato non-goal.

Quindi il piano non garantisce il goal.

Questo esempio e' importante per capire che una state-action table non deve contenere tutte le azioni del dominio, ma deve contenere abbastanza azioni per evitare blocchi sbagliati.

29. Planning problem formale

Dato un dominio:

$$D=(P,S,A,R),$$

un problema di planning e' una tripla:

$$(D,I,G),$$

dove:

• $I\subseteq S$ e' l'insieme degli stati iniziali;
• $G\subseteq S$ e' l'insieme degli stati goal.

La richiesta generale e':

trovare una state-action table $SA$ tale che, partendo da ogni stato in $I$, si riesca a raggiungere uno stato in $G$ nel senso richiesto dalla nozione di soluzione scelta.

Il "nel senso richiesto" e' importante, perche' weak, strong e strong-cyclic hanno garanzie diverse.

30. Le due forme di non determinismo nella definizione

Gli appunti sottolineano due forme di non determinismo:

1. incertezza sugli stati iniziali;
2. non determinismo nella relazione di transizione.

Incertezza sugli iniziali

Se non conosco il colore del semaforo all'inizio, devo includere due stati:

$$(station,red),\quad (station,green).$$

Il piano deve tenere conto di entrambi.

Non determinismo delle transizioni

Se eseguo wait al semaforo rosso, il semaforo potrebbe:

• diventare verde;
• restare rosso.

Allora la stessa azione nello stesso stato ha piu' successori.

31. Requisito di raggiungibilita'

Le soluzioni del planning problem soddisfano un requisito di reachability:

partendo dagli stati iniziali, il piano deve permettere o garantire di raggiungere uno stato goal.

Ma ci sono diversi gradi di garanzia.

La domanda diventa:

• basta che esista un cammino buono?
• devono essere buoni tutti i cammini?
• posso ammettere cicli se sotto fairness prima o poi ne esco?

Queste tre domande danno weak, strong e strong-cyclic.

32. Soluzioni deterministiche: setting

Per prima cosa gli appunti definiscono le soluzioni nel caso in cui $SA$ sia deterministica.

Abbiamo:

• dominio $D=(P,S,A,R)$;
• problema $(D,I,G)$;
• state-action table deterministica $SA$;
• execution structure $K=(Q,T)$ indotta da $SA$ da $I$.

Ora classifichiamo $SA$.

33. Weak solution

$SA$ e' una weak solution se:

per ogni stato iniziale $i\in I$, qualche stato terminale di $K$ appartenente a $G$ e' raggiungibile.

In forma intuitiva:

$$\forall i\in I,\ \exists \text{ path da } i \text{ a un goal}.$$

E' una garanzia esistenziale.

Significa:

• c'e' almeno un modo di arrivare al goal;
• ma possono esistere anche esecuzioni che falliscono;
• il piano non e' robusto rispetto a tutti gli esiti.

Per questo si chiama weak.

34. Perche' weak non basta sempre

Nel semaforo, una soluzione weak potrebbe dire:

se al semaforo aspetto, esiste un'evoluzione in cui il semaforo diventa verde, poi trasporto e arrivo all'aeroporto.

Ma se il semaforo resta rosso per sempre, il piano non raggiunge il goal.

Quindi weak e' utile per dire "il goal e' possibile", non "il goal e' garantito".

35. Strong solution

$SA$ e' una strong solution se:

1. $K$ e' aciclica;
2. tutti gli stati terminali di $K$ sono in $G$.

La condizione di aciclicita' garantisce che non ci siano esecuzioni infinite che girano senza raggiungere il goal.

La condizione sui terminali garantisce che, se l'esecuzione si ferma, si ferma solo in un goal.

Quindi una strong solution garantisce:

$$\forall \text{ path},\ \text{prima o poi si raggiunge }G.$$

E' la nozione piu' robusta.

36. Perche' strong e' forte

Strong elimina due problemi:

1. terminali non-goal;
2. cicli infiniti non-goal.

Se il dominio e' non deterministico, strong richiede che tutti gli esiti ammessi siano compatibili con il raggiungimento del goal.

Nel semaforo, una strong solution sarebbe difficile se l'ambiente potesse mantenere il semaforo rosso per sempre. In quel caso il piano non puo' forzare il verde.

37. Strong-cyclic solution

$SA$ e' una strong-cyclic solution se:

1. da ogni stato $q\in Q$ qualche stato terminale di $K$ e' raggiungibile;
2. tutti gli stati terminali di $K$ sono in $G$.

Rispetto a strong, manca l'obbligo di aciclicita'.

Quindi sono ammessi cicli.

L'idea e':

da ogni stato raggiungibile resta sempre possibile arrivare al goal.

38. Perche' strong-cyclic usa fairness

Una strong-cyclic solution puo' produrre esecuzioni infinite.

Esempio:

• sono al semaforo rosso;
• faccio wait;
• il semaforo resta rosso;
• faccio wait;
• il semaforo resta rosso;
• e cosi' via.

Formalmente esiste un path infinito che non raggiunge il goal.

Perche' allora la soluzione viene considerata accettabile?

Perche' si assume una forma di fairness:

se da un ciclo resta sempre possibile prendere un'uscita favorevole, l'ambiente non puo' ignorarla per sempre in modo ingiusto.

Nel semaforo:

se aspettando il verde prima o poi puo' comparire, una sequenza in cui il verde viene evitato per sempre e' considerata unfair.

Questa e' una strategia di trial and error: provi, osservi, riprovi; sotto fairness prima o poi l'esito favorevole accade.

39. Strong-cyclic non significa strong

Strong-cyclic non garantisce il goal su tutti i path grezzi.

Garantisce il goal su path considerati fair, oppure garantisce che ogni prefisso parziale possa essere esteso a una computazione finita che arriva al goal.

Questa e' la frase da ricordare:

strong-cyclic accetta cicli, ma solo cicli da cui il goal rimane raggiungibile.

Se esiste un ciclo chiuso senza uscita verso il goal, non e' strong-cyclic.

40. Inclusione tra le classi

Le classi soddisfano:

$$\text{strong}\subseteq \text{strong-cyclic}\subseteq \text{weak}.$$

Perche'?

Strong implica strong-cyclic

Se un piano e' strong:

• tutti i path sono finiti;
• tutti i terminali sono goal.

Allora da ogni stato raggiungibile un goal e' raggiungibile, e tutti i terminali sono goal. Quindi e' anche strong-cyclic.

Strong-cyclic implica weak

Se un piano e' strong-cyclic:

• da ogni stato raggiungibile, quindi anche da ogni iniziale, un terminale goal e' raggiungibile.

Quindi esiste almeno un path verso il goal. Questo basta per weak.

Le inclusioni sono proprie

Weak puo' fallire su alcuni esiti.

Strong-cyclic puo' avere cicli infiniti unfair.

Strong non ammette questi cicli.

41. Determinizzazione di una state-action table

Ora passiamo al caso in cui $SA$ sia non deterministica, cioe' possa contenere piu' azioni per lo stesso stato.

Una determinization di $SA$ e' una tabella deterministica:

$$SA'\subseteq SA$$

tale che conserva gli stessi stati coperti:

$$\{s\mid \exists a.\ (s,a)\in SA'\}=\{s\mid \exists a.\ (s,a)\in SA\}.$$

In parole:

per ogni stato in cui $SA$ propone azioni, $SA'$ ne sceglie una sola.

La determinizzazione elimina l'ambiguita' della scelta del piano.

42. Soluzioni non deterministiche

Gli appunti definiscono cosi' le soluzioni per una state-action table non deterministica:

$SA$ e' weak, strong o strong-cyclic se tutte le sue determinizations sono weak, strong o strong-cyclic rispettivamente.

Quindi non basta che una scelta interna alla tabella funzioni.

Deve funzionare ogni modo deterministico di risolvere le scelte ammesse da $SA$.

Questo rende la definizione robusta: se la tabella lascia piu' opzioni, nessuna opzione ammessa deve rovinare la garanzia dichiarata.

43. Esempio di determinizzazione

Supponiamo:

$$SA=\{(s,a),(s,b),(t,c)\}.$$

Allora due determinizations possibili sono:

$$SA_1=\{(s,a),(t,c)\},$$

$$SA_2=\{(s,b),(t,c)\}.$$

Se $SA_1$ e' strong ma $SA_2$ non lo e', allora $SA$ non e' strong.

Il motivo e' semplice:

se il piano ammette anche l'azione $b$ in $s$, allora deve essere sicuro anche scegliere $b$.

44. Perche' servono algoritmi simbolici

Il dominio puo' avere moltissimi stati.

Se ho $n$ variabili booleane, il numero massimo di stati e':

$$2^n.$$

Se alcune variabili hanno piu' valori, la crescita resta combinatoria.

Enumerare tutto il grafo puo' diventare impraticabile.

Il symbolic model checking evita l'enumerazione esplicita rappresentando:

• insiemi di stati;
• relazioni di transizione;
• piani;

come formule booleane, spesso tramite OBDD o strutture simili.

45. Preimmagini: idea generale

Gli algoritmi di planning simbolico ragionano all'indietro dal goal.

Invece di chiedere:

da dove posso andare?

chiedono:

da quali stati posso arrivare nell'insieme gia' buono?

Questo e' il concetto di preimage.

Se $X$ e' un insieme di stati gia' considerati buoni, una preimage calcola stati che possono entrare in $X$ con una certa garanzia.

E' la stessa idea di:

• predecessori in CTL;
• backward reachability;
• attractor nei giochi.

46. Weak preimage

La weak preimage di $X$ contiene gli stati da cui esiste un'azione con almeno un successore in $X$.

Formalmente:

$$Pre_w(X)=\{s\mid \exists a.\ \exists s'.\ R(s,a,s')\land s'\in X\}.$$

Questa e' esistenziale sia sull'azione sia sul successore.

Significa:

c'e' un modo favorevole per entrare in $X$.

Per questo corrisponde alla logica weak.

47. Strong preimage

La strong preimage di $X$ contiene gli stati da cui esiste un'azione tale che tutti i successori possibili stanno in $X$.

Formalmente:

$$Pre_s(X)=\{s\mid \exists a.\ enabled(s,a)\land \forall s'.\ R(s,a,s')\Rightarrow s'\in X\}.$$

Questa e' esistenziale sull'azione, ma universale sugli esiti.

Significa:

posso scegliere un'azione che mi porta sicuramente dentro $X$, qualunque esito non deterministico accada.

Questa e' la base delle strong solutions.

48. Perche' serve enabled o APPL

Nella formula della strong preimage compare una condizione di applicabilita':

$$APPL(s,a)=\exists s'.\ R(s,a,s').$$

Serve per evitare una verita' vacua.

Senza APPL, la formula:

$$\forall s'.\ R(s,a,s')\Rightarrow s'\in X$$

sarebbe vera anche per un'azione non abilitata, perche' non ci sono successori che violano la condizione.

Ma un'azione non abilitata non puo' essere scelta in un piano.

Quindi strong preimage deve richiedere:

• l'azione e' applicabile;
• tutti i suoi successori sono buoni.

49. Strong-cyclic preimage

Per strong-cyclic serve una condizione intermedia.

L'idea e':

scegli azioni che restano dentro una regione controllata e che hanno almeno una possibilita' di progresso verso la regione gia' buona.

Una forma utile e':

$$Pre_{sc}(X,Z)=\{s\mid \exists a.\ Succ(s,a)\subseteq Z\land Succ(s,a)\cap X\ne\emptyset\}.$$

Dove:

• $Z$ e' la regione candidata sicura;
• $X$ e' la parte gia' nota come progressiva verso il goal;
• $Succ(s,a)=\{s'\mid R(s,a,s')\}$.

Questa formula cattura l'idea trial-and-error:

• tutti gli esiti restano nella regione da cui il goal resta possibile;
• almeno un esito fa progresso.

Sotto fairness, ripetere tentativi che hanno sempre una possibilita' di progresso permette di giustificare strong-cyclic.

50. Algoritmo weak: intuizione

Per weak planning si puo' partire da:

$$X_0=G.$$

Poi si aggiungono stati che possono raggiungere $X_i$ con una weak preimage:

$$X_{i+1}=X_i\cup Pre_w(X_i).$$

Quando il punto fisso si stabilizza, $X$ contiene gli stati da cui esiste un path verso il goal.

Se:

$$I\subseteq X,$$

allora esiste una weak solution.

Durante il calcolo si memorizzano anche le coppie $(s,a)$ che giustificano l'ingresso di $s$ in $X$. Quelle coppie costruiscono la state-action table.

51. Algoritmo strong: intuizione

Per strong planning si usa la strong preimage.

Parti da:

$$X_0=G.$$

Poi:

$$X_{i+1}=X_i\cup Pre_s(X_i).$$

Uno stato entra solo se esiste un'azione che forza tutti i successori dentro l'insieme gia' controllato.

Se alla fine:

$$I\subseteq X,$$

allora il piano puo' garantire il goal.

Intuitivamente, costruisci una distanza simbolica dal goal:

• goal a distanza 0;
• stati che forzano il goal a distanza 1;
• stati che forzano stati di distanza minore a distanza 2;
• ecc.

Questo produce una struttura aciclica se il piano sceglie azioni secondo il livello decrescente verso il goal.

52. Algoritmo strong-cyclic: intuizione

Strong-cyclic e' piu' delicato perche' ammette cicli.

L'algoritmo cerca una regione $Z$ tale che:

• da ogni stato in $Z$ il goal resta raggiungibile;
• le azioni scelte non escono da $Z$;
• non ci sono terminali non-goal;
• il progresso verso $G$ e' sempre possibile sotto fairness.

Una descrizione intuitiva e':

1. considera una regione candidata di stati ammessi;
2. calcola quali stati possono raggiungere il goal restando nella regione;
3. elimina stati che non hanno azioni sicure/progressive;
4. ripeti fino a un punto fisso.

Se tutti gli iniziali restano nella regione finale, esiste una strong-cyclic solution.

Questa e' una via di mezzo tra:

• reachability esistenziale;
• garanzia universale forte;
• ragionamento da gioco con fairness.

53. Rappresentazione simbolica del dominio

Per rappresentare simbolicamente il dominio:

1. si associa una variabile booleana a ogni proposizione in $P$;
2. uno stato e' rappresentato da un vettore di variabili;
3. un insieme di stati e' rappresentato da una formula;
4. le azioni sono rappresentate da variabili di azione;
5. i successori sono rappresentati con variabili next-state.

Se il vettore di stato e':

$$\vec{x}=(x_1,\ldots,x_n),$$

allora il vettore next-state e':

$$\vec{x}'=(x'_1,\ldots,x'_n).$$

La relazione di transizione diventa:

$$R(\vec{x},\vec{a},\vec{x}').$$

54. Formula di uno stato

Dato uno stato $s$, la formula $\xi(s)$ e' la congiunzione:

• delle variabili vere in $s$;
• delle negazioni delle variabili false in $s$.

Esempio:

se:

$$s=\{station,red\},$$

allora:

$$\xi(s)=station\land red\land \neg traffic\_light\land \neg airport\land \neg green.$$

Naturalmente, nella pratica si usano codifiche piu' compatte, ma l'idea e' questa.

55. Formula di un insieme di stati

Un insieme $Q\subseteq S$ si rappresenta come:

$$\xi(Q)=\bigvee_{s\in Q}\xi(s).$$

Questa formula e' vera esattamente negli stati appartenenti a $Q$.

Il punto simbolico e':

invece di manipolare una lista di stati, manipolo una formula.

Con OBDD, SAT o altre strutture, questa formula puo' essere gestita in modo compatto.

56. Variabili di azione

Le azioni possono essere rappresentate in due modi.

Una variabile per azione

Si introduce una variabile booleana per ogni azione.

Esempio:

• do_transport;
• do_wait.

Se non sono ammesse azioni concorrenti, bisogna aggiungere vincoli di mutua esclusione:

non possono essere vere due azioni contemporaneamente.

Codifica binaria delle azioni

Se ci sono $|A|$ azioni, si possono usare:

$$\lceil \log_2 |A| \rceil$$

variabili booleane.

Ogni assegnamento rappresenta un'azione.

In questo caso la mutua esclusione e' incorporata nella codifica, perche' un assegnamento denota una sola azione.

57. Relazione di transizione simbolica

Una transizione e' una tripla:

$$(s,a,s').$$

Simbolicamente viene rappresentata con:

$$R(\vec{x},\vec{a},\vec{x}').$$

Dove:

• $\vec{x}$ descrive lo stato corrente;
• $\vec{a}$ descrive l'azione scelta;
• $\vec{x}'$ descrive lo stato successivo.

Questa e' la stessa forma usata nel symbolic model checking del capitolo 9.

58. Formule principali

Gli appunti indicano formule per rappresentare:

• stati validi: $S(\vec{x})$;
• transizione: $R(\vec{x},\vec{a},\vec{x}')$;
• iniziali: $I(\vec{x})$;
• goal: $G(\vec{x})$.

Il planning problem diventa allora manipolazione di formule:

• calcolo preimmagini;
• verifica se gli iniziali sono inclusi nella regione vincente;
• estrazione delle azioni che giustificano il piano.

59. Rappresentazione simbolica di una state-action table

Una state-action table $SA$ si rappresenta con una formula:

$$SA(\vec{x},\vec{a}).$$

Questa formula e' vera quando:

nello stato rappresentato da $\vec{x}$, il piano ammette l'azione rappresentata da $\vec{a}$.

Da questa formula si possono ottenere:

Stati coperti dalla tabella

$$StatesOf(SA)(\vec{x})=\exists \vec{a}.\ SA(\vec{x},\vec{a}).$$

Azioni associate a uno stato

Per uno stato fissato $s$, le azioni ammesse sono quelle $\vec{a}$ tali che:

$$SA(\xi(s),\vec{a})$$

risulta vera.

60. Preimmagini simboliche come costruttori di piani

La cosa importante negli appunti e':

le preimmagini non restituiscono solo insiemi di stati; possono costruire anche state-action tables.

Per weak preimage, si memorizzano coppie $(s,a)$ per cui:

$$\exists s'.\ R(s,a,s')\land Q(s').$$

Per strong preimage, si memorizzano coppie $(s,a)$ per cui:

$$APPL(s,a)\land \forall s'.\ R(s,a,s')\Rightarrow Q(s').$$

Quindi l'algoritmo non dice solo "da qui si puo' vincere", ma anche:

quale azione usare per giustificare la vittoria.

Questo e' il passaggio da verifica a sintesi del piano.

61. Weak preimage simbolica

Con vettori:

• stato corrente $\vec{x}$;
• azione $\vec{a}$;
• stato successivo $\vec{x}'$;
• regione target $Q(\vec{x}')$;

la weak preimage usa:

$$\exists \vec{x}'.\ R(\vec{x},\vec{a},\vec{x}')\land Q(\vec{x}').$$

Se poi voglio solo l'insieme degli stati, quantifico anche le azioni:

$$\exists \vec{a}.\exists \vec{x}'.\ R(\vec{x},\vec{a},\vec{x}')\land Q(\vec{x}').$$

Se invece voglio la state-action table, tengo anche $\vec{a}$ libera.

62. Strong preimage simbolica

La strong preimage usa:

$$APPL(\vec{x},\vec{a})\land \forall \vec{x}'.\ R(\vec{x},\vec{a},\vec{x}')\Rightarrow Q(\vec{x}').$$

Dove:

$$APPL(\vec{x},\vec{a})=\exists \vec{x}'.\ R(\vec{x},\vec{a},\vec{x}').$$

La lettura e':

• l'azione e' applicabile;
• ogni successore ammesso dalla relazione entra nella regione target.

Questa e' la formula simbolica della garanzia forte.

63. Collegamento con CTL

Le nozioni weak e strong ricordano formule CTL:

• weak: esiste un cammino verso il goal, simile a $EF\ goal$;
• strong: tutti i cammini raggiungono il goal, simile a $AF\ goal$;
• strong-cyclic: da ogni stato resta possibile raggiungere il goal, con una lettura fair/trial-and-error.

Ma attenzione:

nel planning non stiamo solo verificando una formula su un modello dato; stiamo scegliendo una state-action table che induce il modello da verificare.

Quindi CTL aiuta a capire il significato, ma il problema operativo e' di sintesi.

64. Il linguaggio di descrizione delle azioni $\mathcal{AR}$

Gli appunti introducono il linguaggio $\mathcal{AR}$ per modellare domini di planning non deterministici.

Le forme principali sono:

• A CAUSES P IF Q;
• A POSSIBLY CHANGES F IF Q;
• ALWAYS P;
• INITIALLY P;
• GOAL G.

Questo linguaggio serve a descrivere il dominio in modo dichiarativo, poi tradurlo in formule booleane e relazioni di transizione.

65. A CAUSES P IF Q

La regola:

A CAUSES P IF Q

significa:

se l'azione $A$ viene eseguita in uno stato in cui vale $Q$, allora nel successore deve valere $P$.

Esempio:

transportation CAUSES traffic_light IF station

Se sono alla stazione e faccio transportation, nel prossimo stato sono al semaforo.

66. A POSSIBLY CHANGES F IF Q

La regola:

A POSSIBLY CHANGES F IF Q

significa:

se eseguo $A$ in una situazione in cui vale $Q$, allora il fluent $F$ puo' cambiare.

Questo introduce non determinismo.

Esempio:

wait POSSIBLY CHANGES light IF traffic_light

Se aspetto al semaforo, il colore puo' cambiare, ma non e' garantito che cambi nel modo desiderato.

67. ALWAYS P

La regola:

ALWAYS P

impone un vincolo di integrita' su tutti gli stati validi.

Esempio:

ALWAYS station <-> not (traffic_light or airport)

Serve a dire che la posizione e' mutuamente esclusiva:

• o station;
• o traffic_light;
• o airport.

Non posso essere in due posizioni allo stesso tempo.

68. INITIALLY P e GOAL G

La regola:

INITIALLY P

descrive gli stati iniziali.

La regola:

GOAL G

descrive gli stati goal.

Esempio:

INITIALLY station
GOAL airport

Questo non fissa necessariamente il colore del semaforo, quindi possono esserci piu' stati iniziali e piu' stati goal.

69. Formalizzazione dell'esempio in $\mathcal{AR}$

Una formalizzazione compatta dell'esempio e':

transportation CAUSES traffic_light IF station
transportation CAUSES airport IF traffic_light and light = green
transportation CAUSES false IF not (station or (traffic_light and light = green))
wait CAUSES false IF not traffic_light
ALWAYS station <-> not (traffic_light or airport)
ALWAYS traffic_light <-> not (station or airport)
ALWAYS airport <-> not (traffic_light or station)
INITIALLY station
GOAL airport

Le righe con CAUSES false esprimono impossibilita' o azioni non applicabili.

Per esempio:

• non puoi trasportare se non sei alla stazione o al semaforo verde;
• non puoi aspettare se non sei al semaforo.

70. Stati validi in $\mathcal{AR}$

Gli stati validi sono le valutazioni che soddisfano tutti i vincoli ALWAYS.

Quindi ALWAYS definisce:

$$State(\vec{x}).$$

Gli stati iniziali soddisfano in piu':

$$Initially(\vec{x}).$$

Gli stati goal soddisfano in piu':

$$Goal(\vec{x}).$$

Quindi:

$$I(\vec{x})=State(\vec{x})\land Initially(\vec{x}),$$

$$G(\vec{x})=State(\vec{x})\land Goal(\vec{x}).$$

71. Azioni in $\mathcal{AR}$

Le azioni vengono rappresentate con variabili di azione.

Una variabile e' vera se l'azione corrispondente viene eseguita.

Se non voglio azioni concorrenti, impongo che esattamente una azione sia vera, o al piu' una, a seconda della modellazione.

Questo permette di tradurre le regole di $\mathcal{AR}$ in una formula:

$$R(\vec{x},\vec{a},\vec{x}').$$

72. Effetti e next-state

Una regola:

A CAUSES P IF Q

diventa un vincolo sul prossimo stato:

se nello stato corrente vale $Q$ e l'azione $A$ e' scelta, allora nel next-state vale $P$.

In forma schematica:

$$A(\vec{a})\land Q(\vec{x})\Rightarrow P(\vec{x}').$$

Il punto e':

• $Q$ guarda lo stato corrente;
• $P$ guarda lo stato successivo;
• $A$ guarda l'azione scelta.

73. Inerzia e frame problem

Per i fluents inerziali bisogna impedire cambiamenti immotivati.

Se un fluent $F$ e' inerziale, allora:

$F$ puo' cambiare solo se un'azione lo causa o se una regola POSSIBLY CHANGES lo permette.

Senza vincoli di inerzia, il modello ammetterebbe transizioni assurde:

• il pacco cambia posizione senza transport;
• una porta si apre senza open;
• una risorsa sparisce senza evento o azione.

Gli appunti collegano questo alla preservazione nei sistemi di transizione:

cio' che non viene modificato resta uguale.

74. Perche' POSSIBLY CHANGES e' diverso da CAUSES

CAUSES impone un effetto.

POSSIBLY CHANGES permette un cambiamento.

Differenza:

• A CAUSES P IF Q: se $A$ e $Q$, allora $P$ nel successore;
• A POSSIBLY CHANGES F IF Q: se $A$ e $Q$, allora $F$ puo' cambiare, ma non e' obbligato a cambiare in un valore specifico.

Quindi POSSIBLY CHANGES e' una sorgente di non determinismo.

75. Collegamento con i capitoli precedenti

Il capitolo 11 riusa quasi tutti gli strumenti gia' visti.

Dal capitolo 4: FTS e fairness

Strong-cyclic usa fairness per escludere esecuzioni infinitamente sfortunate.

Dal capitolo 7: CTL e LTL

Weak e strong ricordano $EF$ e $AF$.

Extended goals possono essere formule temporali.

Dal capitolo 8: procedure di model checking

Le preimmagini e i punti fissi sono la base degli algoritmi.

Dal capitolo 9: symbolic model checking

Stati, transizioni e piani vengono rappresentati con formule booleane.

Dal capitolo 10: sintesi

Il risultato non e' solo una verifica, ma un controller/piano eseguibile.

76. Errori tipici all'esame

Confondere piano e path

Un path e' una singola esecuzione.

Un piano e' una regola che genera possibili esecuzioni.

Nel non determinismo, lo stesso piano puo' avere molti path.

Dire che weak garantisce il goal

Weak garantisce solo che esiste un path verso il goal.

Non garantisce tutti gli esiti.

Dire che strong-cyclic e' uguale a strong

No. Strong-cyclic ammette cicli.

La garanzia dipende dall'ipotesi di fairness.

Dimenticare terminali non-goal

Un piano che si blocca in uno stato non-goal non e' strong e non e' strong-cyclic.

Dimenticare APPL nella strong preimage

Senza applicabilita', un'azione non enabled potrebbe soddisfare vacuamente la condizione universale.

Confondere non determinismo del piano e non determinismo del dominio

Il piano e' non deterministico se ammette piu' azioni nello stesso stato.

Il dominio e' non deterministico se la stessa azione nello stesso stato ha piu' successori.

77. Mini-esempio: classificazione rapida

Supponi:

• stato iniziale $s_0$;
• goal $g$;
• stato morto $d$;
• azione $a$ da $s_0$ con due successori: $g$ e $d$.

Se il piano contiene solo $(s_0,a)$:

• e' weak, perche' esiste l'esito verso $g$;
• non e' strong, perche' esiste l'esito verso $d$;
• non e' strong-cyclic se $d$ e' terminale non-goal.

Ora supponi invece:

• da $s_0$ con try puoi tornare a $s_0$ o andare a $g$;
• $g$ e' terminale goal.

Il piano che ripete try:

• non e' strong, perche' esiste il path infinito $s_0,s_0,s_0,\ldots$;
• e' strong-cyclic sotto fairness, perche' da $s_0$ il goal resta sempre raggiungibile;
• e' weak.

78. Esercizio 1: weak o strong?

Hai:

• $I=\{s\}$;
• $G=\{g\}$;
• azione $a$ da $s$ con successori $g$ e $t$;
• $t$ terminale non-goal.

Il piano $SA=\{(s,a)\}$ e' strong?

Risposta: no.

Motivo: un successore possibile e' $t$, terminale non-goal. Strong richiede che tutti i terminali siano goal e che tutti i path arrivino al goal.

E' weak?

Si', perche' esiste un path da $s$ a $g$.

79. Esercizio 2: strong-cyclic

Hai:

• $s$ iniziale;
• $g$ goal;
• azione try da $s$ con successori $s$ e $g$.

Il piano $SA=\{(s,try)\}$ e' strong?

No, perche' esiste il path infinito che resta in $s$.

E' strong-cyclic?

Si', se tutti i terminali sono goal e se da $s$ il goal resta raggiungibile. Sotto fairness, l'esito favorevole non puo' essere evitato per sempre.

80. Esercizio 3: strong preimage

Sia:

$$X=\{g\}.$$

Da $s$:

• azione $a$ ha successori $\{g\}$;
• azione $b$ ha successori $\{g,d\}$.

Quali azioni giustificano la strong preimage di $X$?

Solo $a$.

Per $b$, non tutti i successori sono in $X$.

81. Esercizio 4: weak preimage

Con lo stesso esempio:

• $a$ ha successori $\{g\}$;
• $b$ ha successori $\{g,d\}$.

Quali azioni giustificano la weak preimage di $X$?

Sia $a$ sia $b$, perche' entrambe hanno almeno un successore in $X$.

82. Esercizio 5: determinizzazione

Sia:

$$SA=\{(s,a),(s,b),(t,c)\}.$$

Elenca le determinizations.

Risposta:

$$SA_1=\{(s,a),(t,c)\},$$

$$SA_2=\{(s,b),(t,c)\}.$$

Se $SA_1$ e' weak e $SA_2$ non e' weak, allora $SA$ e' weak?

No. Per una tabella non deterministica, tutte le determinizations devono avere la proprieta'.

83. Mappa orale del capitolo

Per esporre il capitolo 11 all'esame:

1. parti dal planning problem intuitivo;
2. spiega action-based planning;
3. definisci fluents, stati, azioni, iniziali e goal;
4. distingui fluents inerziali e non inerziali;
5. spiega le sorgenti di non determinismo;
6. classifica situated, universal e conformant plans;
7. definisci il dominio $D=(P,S,A,R)$;
8. spiega action enabled;
9. presenta l'esempio pacco-semaforo;
10. definisci state-action table;
11. costruisci la execution structure $K=(Q,T)$;
12. definisci terminali, execution path e aciclicita';
13. definisci planning problem $(D,I,G)$;
14. confronta weak, strong e strong-cyclic;
15. spiega la fairness in strong-cyclic;
16. passa alle determinizations;
17. spiega preimmagini weak e strong;
18. mostra la rappresentazione simbolica;
19. chiudi con $\mathcal{AR}$ e le regole CAUSES, POSSIBLY CHANGES, ALWAYS, INITIALLY, GOAL.

84. Risposta orale completa

Una risposta compatta ma completa potrebbe essere:

Nel planning non deterministico via symbolic model checking rappresentiamo il dominio come $D=(P,S,A,R)$, dove $P$ e' un insieme finito di proposizioni, $S\subseteq 2^P$ e' l'insieme degli stati, $A$ e' l'insieme delle azioni e $R\subseteq S\times A\times S$ e' la relazione di transizione. Un'azione e' enabled in uno stato se ha almeno un successore secondo $R$. Un problema di planning e' una tripla $(D,I,G)$, con stati iniziali e goal. Un piano e' rappresentato come state-action table $SA\subseteq S\times A$; da questa tabella si costruisce la execution structure $K=(Q,T)$, cioe' il grafo delle esecuzioni possibili del piano a partire da $I$.

Le soluzioni si distinguono in weak, strong e strong-cyclic. Una weak solution richiede che da ogni iniziale esista almeno un path verso un terminale goal. Una strong solution richiede che la execution structure sia aciclica e che tutti i terminali siano goal, quindi tutti i cammini terminano correttamente. Una strong-cyclic solution ammette cicli, ma richiede che da ogni stato raggiungibile un terminale goal resti raggiungibile e che tutti i terminali siano goal; la garanzia vale sotto fairness. Per tabelle non deterministiche, la proprieta' deve valere per tutte le determinizations.

Il collegamento con il symbolic model checking consiste nel rappresentare stati, azioni, transizioni, iniziali, goal e piani con formule booleane: $S(\vec{x})$, $R(\vec{x},\vec{a},\vec{x}')$, $I(\vec{x})$, $G(\vec{x})$ e $SA(\vec{x},\vec{a})$. Gli algoritmi lavorano all'indietro dal goal con preimmagini. La weak preimage usa una condizione esistenziale sui successori; la strong preimage richiede un'azione applicabile i cui successori siano tutti nella regione target. In questo modo non solo si verifica la raggiungibilita', ma si costruisce anche la state-action table che realizza il piano.

85. Riassunto finale

Il capitolo 11 dice:

• il planning e' costruzione di piani, non solo verifica di modelli;
• un piano in domini non deterministici e' una state-action table;
• la execution structure mostra tutte le esecuzioni indotte dal piano;
• weak, strong e strong-cyclic misurano livelli diversi di garanzia;
• strong-cyclic accetta trial-and-error sotto fairness;
• le determinizations servono a interpretare tabelle non deterministiche;
• il symbolic model checking rappresenta tutto con formule booleane;
• le preimmagini costruiscono regioni vincenti e azioni del piano;
• $\mathcal{AR}$ descrive azioni, effetti, vincoli, iniziali e goal in modo dichiarativo.

Se ricordi solo una frase:

il planning non deterministico via symbolic model checking trasforma la ricerca di un piano in un calcolo simbolico di stati e azioni che garantiscono, in modo weak, strong o strong-cyclic, il raggiungimento del goal.