Logica temporale lineare - Riassunto

Punti chiave

• LTL descrive proprieta su una singola sequenza lineare infinita di stati.
• La sintassi combina lettere proposizionali, connettivi booleani e operatori temporali come $X$, $F$, $G$ e $U$.
• Esistono varianti dell'Until: forte, debole, stretto e non stretto.
• La soddisfacibilita LTL puo essere decisa tramite tableau costruiti su atomi della formula e sottografi fortemente connessi realizzanti.
• Le formule LTL possono essere tradotte in automi di Buchi, rendendo possibile il model checking automata-theoretic.

Argomento centrale

Tradurre LTL in automi consente di ridurre la verifica di proprieta temporali a problemi su linguaggi e prodotti di automi.

Rilevanza per V&V in AI

LTL e' adatta a specificare safety, liveness e fairness di agenti e sistemi reattivi.

Logica ad albero computazionale (CTL) - Riassunto

Punti chiave

• CTL e' una logica temporale branching-time: valuta proprieta su alberi di computazioni possibili.
• A differenza di LTL, CTL usa quantificatori di cammino: $A$ per tutti i cammini ed $E$ per almeno un cammino.
• CTL distingue formule di stato e formule di cammino: gli operatori temporali devono essere combinati con un quantificatore di cammino.
• Gli operatori principali sono $X$, $F$, $G$ e $U$, sempre nella forma quantificata, ad esempio $EF p$ o $AG p$.
• CTL e LTL sono incomparabili: CTL esprime bene proprieta di possibilita, LTL esprime naturalmente molte proprieta di fairness.

Argomento centrale

CTL e' adatta al model checking efficiente perche le formule possono essere valutate localmente sugli stati, spesso tramite algoritmi di labeling e punti fissi.

Rilevanza per V&V in AI

CTL permette di specificare proprieta su sistemi non deterministici, ad esempio: da ogni stato deve restare possibile raggiungere una condizione sicura.

Logica temporale lineare (LTL)

LTL e' una logica temporale lineare: interpreta le formule su singole sequenze infinite di stati.

Sintassi

Sia $AP$ l'insieme delle proposizioni atomiche, come request, grant, safe o error.

La grammatica base e': $$\varphi ::= p \mid \neg\varphi \mid \varphi\land\psi \mid X\varphi \mid \varphi U \psi$$

dove $p\in AP$.

Significa che: - una proposizione atomica e' una formula; - se $\varphi$ e' una formula, allora anche $\neg\varphi$, $X\varphi$, $F\varphi$ e $G\varphi$ sono formule; - se $\varphi$ e $\psi$ sono formule, allora anche $\varphi\land\psi$, $\varphi\lor\psi$, $\varphi\to\psi$ e $\varphi U \psi$ sono formule.

$F$ e $G$ sono abbreviazioni utili: $$F\varphi := true\ U\ \varphi$$ $$G\varphi := \neg F\neg\varphi$$

Le parentesi contano. $G(request\to F grant)$ significa che ogni richiesta, in qualunque istante, verra' prima o poi servita. Senza il $G$ esterno, $request\to F grant$ controlla solo la posizione corrente.

Operatori principali

• $X\varphi$: $\varphi$ vale nel prossimo stato;
• $F\varphi$: $\varphi$ vale prima o poi;
• $G\varphi$: $\varphi$ vale sempre;
• $\varphi U \psi$: $\varphi$ vale fino al momento in cui vale $\psi$.

Uso nel model checking

Una specifica LTL descrive comportamenti ammessi o vietati lungo le computazioni. Spesso si traduce la negazione della formula in un automa di Buchi e si cerca un controesempio nel prodotto con il sistema.

Esempi

• Safety: $G\neg bad$.
• Response: $G(req \rightarrow F ack)$.
• Fairness: $GF enabled \rightarrow GF taken$.

Collegamenti

• Automi di Büchi
• Model checking
• Logica ad albero computazionale (CTL)

Logica ad albero computazionale (CTL)

CTL e' una logica temporale branching-time usata per specificare proprieta su sistemi con piu futuri possibili.

Concetti principali

• Tempo ramificato: da uno stato possono partire piu cammini.
• Quantificatori di cammino: $A$ significa tutti i cammini, $E$ significa almeno un cammino.
• Operatori temporali: $X$, $F$, $G$, $U$.
• Formule di stato: in CTL gli operatori temporali sono combinati con quantificatori, ad esempio $AF p$, $EG p$, $E[p U q]$.

CTL vs LTL

CTL puo esprimere proprieta di possibilita, ad esempio $AGEF p$: da ogni stato e' sempre possibile tornare a uno stato con $p$. LTL esprime invece in modo naturale proprieta lungo cammini lineari e molte condizioni di fairness.

Collegamenti

• Logica temporale lineare (LTL)
• Model checking
• Modello di Kripke

Approfondimento completo settimana 4 - Logiche temporali

Questo documento espande il Capitolo 7. L'obiettivo e' capire davvero LTL, CTL e CTL-star: non solo ricordare le sigle, ma saper tradurre requisiti naturali, valutare formule su computazioni e spiegare perche' linear time e branching time non sono la stessa cosa.

Il capitolo 8 entrera' piu a fondo nelle procedure di model checking. Qui pero' anticipiamo i richiami essenziali, perche' all'orale le domande su LTL e CTL quasi sempre scivolano verso:

• semantica precisa degli operatori;
• differenza tra una singola computazione e l'albero di tutte le computazioni;
• esempi di traduzione;
• incomparabilita' tra LTL e CTL;
• collegamento con automi di Buchi e model checking.

0. Idea guida: perche' servono logiche temporali?

La logica proposizionale dice che cosa vale in un singolo istante:

$$ safe,\quad request,\quad grant,\quad error. $$

Per i sistemi reattivi questo non basta. Un sistema reattivo non produce un risultato e poi termina: continua a interagire con l'ambiente. Quindi le proprieta' importanti non parlano solo dello stato corrente, ma dell'evoluzione nel tempo.

Esempi tipici:

• "non si raggiunge mai uno stato cattivo";
• "ogni richiesta viene prima o poi servita";
• "se una transizione resta abilitata, prima o poi viene eseguita";
• "da ogni stato deve restare possibile tornare a una configurazione sicura";
• "esiste almeno una strategia che porta al goal".

Queste frasi hanno due dimensioni:

1. una dimensione temporale: adesso, prossimo stato, prima o poi, sempre, fino a;
2. una dimensione di scelta: guardo una sola computazione oppure tutti i futuri possibili?

LTL e CTL rispondono in modo diverso:

• LTL guarda una computazione lineare alla volta;
• CTL guarda l'albero ramificato delle computazioni possibili;
• CTL-star generalizza entrambe.

1. Richiami dai capitoli precedenti

Da FTS e Kripke ai cammini

Nei capitoli su FTS e SPL hai visto che un sistema puo' essere rappresentato come stati e transizioni. Per le logiche temporali useremo spesso una struttura di Kripke:

$$ M=(S,R,L). $$

Dove:

• $S$ e' un insieme di stati;
• $R$ e' una relazione di transizione tra stati;
• $L$ assegna a ogni stato l'insieme delle proposizioni atomiche vere in quello stato.

Se in uno stato $s$ vale:

$$ L(s)=\{request,ready\}, $$

allora in quello stato sono vere le proposizioni request e ready, mentre sono false le proposizioni non contenute in $L(s)$.

Di solito si assume che la relazione di transizione sia totale: ogni stato ha almeno un successore. Questo evita cammini finiti. Le logiche temporali del corso sono pensate per computazioni infinite.

Un cammino e' una sequenza infinita:

$$ \pi=s0,s1,s2,\ldots $$

tale che per ogni posizione vale:

$$ R(si,s(i+1)). $$

La traccia associata al cammino e' la parola infinita:

$$ L(s0),L(s1),L(s2),\ldots $$

Questa e' la connessione con gli automi di Buchi: un comportamento del sistema e' una parola infinita su alfabeto $2^{AP}$.

Da Buchi a LTL

Nel capitolo 5 hai visto gli automi di Buchi, che riconoscono parole infinite. LTL puo' essere vista come un linguaggio piu comodo per descrivere insiemi di parole infinite.

Una formula come:

$$ G(request \to F grant) $$

descrive il linguaggio di tutte le computazioni in cui ogni richiesta viene prima o poi seguita da un grant.

Poi, per fare model checking, si puo' tradurre la formula LTL in un automa di Buchi.

Da S1S a LTL

Nel capitolo 6 hai visto S1S, che parla di posizioni naturali e insiemi di posizioni. LTL e' meno espressiva di S1S piena, ma molto naturale per specificare proprieta' temporali.

Il teorema di Kamp collega LTL al frammento del primo ordine su ordini lineari discreti. A livello orale basta ricordare questo:

• S1S e automi di Buchi catturano gli omega-regolari;
• LTL cattura un frammento importante e molto usato;
• aggiungere operatori al passato a LTL non aumenta il potere espressivo su tempo lineare discreto, ma puo' rendere le formule piu corte.

La cornice modale: da dove vengono ♢ e ◻

Negli appunti le logiche temporali vengono introdotte come caso particolare della logica modale. L'idea: la logica classica valuta una formula in un unico "mondo"; la logica modale considera un insieme di mondi collegati da una relazione di accessibilita' (un grafo: i nodi sono mondi/stati, gli archi dicono quali mondi sono raggiungibili). Una formula puo' essere vera in un mondo e falsa in un altro. I due operatori classici:

• possibilita' $\Diamond p$: esiste un mondo accessibile dal corrente in cui $p$ e' vera (un $\exists$ sugli archi uscenti);
• necessita' $\Box p$: in tutti i mondi accessibili $p$ e' vera (un $\forall$). Nota: in logica modale "possibilmente vero" non implica "anche falso da qualche parte", a differenza dell'uso in linguaggio naturale.

La logica temporale e' il caso in cui i mondi sono istanti di tempo e l'accessibilita' e' l'ordinamento temporale: $\Diamond$ diventa F (sometime in the future), $\Box$ diventa G (always in the future). Ma attenzione: in LTL l'operatore di base non e' F/G bensi' l'until — F e G si derivano da U, non viceversa.

I parametri di progetto di una logica temporale

Gli appunti elencano le scelte che definiscono una logica temporale; il corso prende sempre la prima opzione di ogni coppia:

Quindi PLTL = proposizionale + clock globale + tempo lineare discreto a punti con istante iniziale (ℕ) + solo futuro: esattamente la forma delle computazioni dei sistemi visti finora.

2. LTL: Linear Temporal Logic

Intuizione

LTL interpreta le formule su una singola sequenza infinita:

$$ \sigma=s0,s1,s2,\ldots $$

oppure, equivalentemente, sulla traccia:

$$ L(s0),L(s1),L(s2),\ldots $$

Quando scrivo:

$$ \sigma,i\models \varphi, $$

intendo:

la formula $\varphi$ e' vera lungo la computazione $\sigma$ alla posizione $i$.

Quando l'indice non e' scritto, di solito si intende la posizione iniziale:

$$ \sigma\models\varphi $$

cioe':

$$ \sigma,0\models\varphi. $$

Sintassi base

Sia $AP$ un insieme finito di proposizioni atomiche. Una proposizione atomica e' un nome che puo' essere vero o falso in uno stato del sistema, per esempio:

$$ request,\quad grant,\quad error,\quad safe,\quad critical. $$

Attenzione: una proposizione atomica non e' una variabile numerica e non e' un'azione. E' un predicato osservabile sullo stato corrente. Se nello stato $s_i$ vale request, allora la traccia in posizione $i$ contiene la proposizione request.

Le formule LTL sono generate da:

$$ \varphi ::= p \mid \neg\varphi \mid \varphi\land\psi \mid X\varphi \mid \varphi U \psi $$

dove $p\in AP$.

Questa riga e' una grammatica induttiva. Significa:

1. ogni proposizione atomica $p$ e' gia' una formula;
2. se $\varphi$ e' una formula, allora anche $\neg\varphi$ e' una formula;
3. se $\varphi$ e $\psi$ sono formule, allora $\varphi\land\psi$ e' una formula;
4. se $\varphi$ e' una formula, allora $X\varphi$ e' una formula;
5. se $\varphi$ e $\psi$ sono formule, allora $\varphi U \psi$ e' una formula.

Tutte le formule LTL si costruiscono ripetendo queste regole un numero finito di volte. Questa e' la cosa importante: una formula LTL e' un oggetto finito che descrive proprieta' di computazioni infinite.

Formule atomiche e formule composte

Le formule piu semplici sono le proposizioni atomiche:

$$ request,\quad grant,\quad safe. $$

Da queste si costruiscono formule piu grandi:

$$ \neg error $$

$$ request\land \neg grant $$

$$ X grant $$

$$ request\ U\ grant. $$

LTL distingue due tipi di operatori:

• operatori booleani, come $\neg,\land,\lor,\to$;
• operatori temporali, come $X,F,G,U$.

Gli operatori booleani combinano verita' nello stesso istante. Gli operatori temporali spostano lo sguardo lungo la computazione.

Operatori unari e binari

Alcuni operatori prendono una sola formula:

$$ \neg\varphi,\quad X\varphi,\quad F\varphi,\quad G\varphi. $$

Questi sono operatori unari.

Altri operatori prendono due formule:

$$ \varphi\land\psi,\quad \varphi\lor\psi,\quad \varphi\to\psi,\quad \varphi U \psi. $$

Questi sono operatori binari.

In breve: gli operatori unari si mettono davanti a una formula; gli operatori binari collegano due formule gia' ben formate.

Questa distinzione evita molti errori sintattici. Ad esempio:

• $G$ da solo non e' una formula;
• $U p$ non e' una formula, perche' $U$ ha bisogno di una formula a sinistra e una a destra;
• $F(p\land q)$ e' una formula;
• $(F p)\land q$ e' una formula diversa.

Parentesi e precedenza

Quando una formula e' lunga, le parentesi servono a dire come deve essere letta. Per evitare ambiguita', puoi usare questa precedenza pratica:

1. operatori unari: $\neg$, $X$, $F$, $G$;
2. operatori temporali binari: $U$, $W$, $R$;
3. congiunzione $\land$;
4. disgiunzione $\lor$;
5. implicazione $\to$.

Quindi:

$$ G request \to F grant $$

si legge normalmente come:

$$ (G request)\to(F grant). $$

Ma spesso quello che si vuole dire e':

$$ G(request\to F grant). $$

Le due formule sono molto diverse.

Perche $G(request\to F grant)$ non e' uguale a $request\to F grant$

La formula:

$$ request\to F grant $$

controlla solo la posizione corrente. Dice: se request vale adesso, allora da adesso in poi prima o poi arrivera' grant.

La formula:

$$ G(request\to F grant) $$

controlla ogni posizione della computazione. Dice: in ogni istante, se c'e' una richiesta, allora da quell'istante in poi arrivera' un grant.

Questa e' la formula corretta per "ogni richiesta viene prima o poi servita". Il $G$ esterno e' necessario perche' la proprieta' deve essere controllata in tutti gli istanti, non solo all'inizio.

Come leggere formule annidate

Gli operatori temporali possono essere annidati.

$$ GF p $$

si legge come:

$$ G(Fp). $$

Significa: in ogni posizione futura, esiste una posizione ancora piu futura in cui vale $p$. In altre parole, $p$ accade infinitamente spesso.

Invece:

$$ FG p $$

si legge come:

$$ F(Gp). $$

Significa: prima o poi si raggiunge un punto dopo il quale $p$ vale sempre.

Quindi $GFp$ e $FGp$ non sono intercambiabili:

• $GFp$: $p$ torna infinite volte;
• $FGp$: da un certo momento in poi $p$ resta sempre vero.

Formule ben formate e formule non ben formate

Esempi di formule LTL ben formate:

$$ G\neg error $$

$$ G(request\to F grant) $$

$$ GF enabled \to GF taken $$

$$ G(reset\to XG safe) $$

$$ \neg grant\ U\ request. $$

Esempi da non scrivere:

• $G\to p$, perche' $G$ deve applicarsi a una formula;
• $p U$, perche' manca la formula a destra di $U$;
• $X U p$, perche' $X$ deve essere seguito da una formula e $U$ deve avere due argomenti;
• $p q$, perche' due proposizioni vicine non formano una formula senza un connettivo.

Sintassi minimale e abbreviazioni

La grammatica base usa solo:

$$ p,\quad \neg,\quad \land,\quad X,\quad U. $$

Questo non significa che in LTL si possano usare solo questi simboli. Significa che gli altri operatori possono essere definiti a partire da questi.

Gli altri connettivi si definiscono come abbreviazioni:

$$ \varphi\lor\psi := \neg(\neg\varphi\land\neg\psi) $$

$$ \varphi\to\psi := \neg\varphi\lor\psi $$

Operatori temporali derivati:

$$ F\varphi := true\;U\;\varphi $$

$$ G\varphi := \neg F\neg\varphi $$

Quindi $F$ e $G$ non sono indispensabili dal punto di vista teorico, ma sono indispensabili dal punto di vista pratico: rendono le specifiche leggibili.

Perche $F$ si definisce con $U$

La definizione:

$$ F\varphi := true\;U\;\varphi $$

dice: "true vale fino al momento in cui arriva $\varphi$". Poiche' true vale sempre, l'unico vincolo reale e' che $\varphi$ arrivi prima o poi.

Quindi $F\varphi$ significa:

prima o poi $\varphi$.

Perche $G$ si definisce con $F$

La definizione:

$$ G\varphi := \neg F\neg\varphi $$

dice: "non accade mai che prima o poi arrivi una violazione di $\varphi$".

Se non esiste nessun futuro in cui $\varphi$ e' falsa, allora $\varphi$ vale sempre.

Quindi $G\varphi$ significa:

da ora in poi, sempre $\varphi$.

Lettura:

• $X\varphi$: nel prossimo stato vale $\varphi$;
• $F\varphi$: prima o poi vale $\varphi$;
• $G\varphi$: da ora in poi vale sempre $\varphi$;
• $\varphi U \psi$: $\varphi$ vale fino al primo momento in cui vale $\psi$, e $\psi$ deve arrivare.

Metodo pratico per scrivere una formula LTL

Quando devi tradurre una frase naturale in LTL, procedi cosi':

1. individua le proposizioni atomiche;
2. chiediti se la proprieta' deve valere solo ora o in ogni istante;
3. scegli l'operatore temporale principale;
4. metti le parentesi prima di semplificare;
5. controlla se stai parlando di un evento singolo, di una risposta, di una permanenza o di ricorrenza.

Esempio:

Frase:

ogni richiesta viene prima o poi servita.

Proposizioni:

$$ request,\quad grant. $$

Evento locale:

$$ request\to F grant. $$

Deve valere in ogni istante:

$$ G(request\to F grant). $$

Questa costruzione e' piu sicura che provare a scrivere subito la formula finale.

Semantica precisa

Sia $\sigma=s0,s1,s2,\ldots$ un cammino e sia $i$ una posizione.

Per le proposizioni:

$$ \sigma,i\models p $$

se e solo se:

$$ p\in L(si). $$

Per i booleani:

$$ \sigma,i\models \neg\varphi $$

se e solo se:

$$ \sigma,i\not\models \varphi. $$

$$ \sigma,i\models \varphi\land\psi $$

se e solo se:

$$ \sigma,i\models\varphi \quad\text{e}\quad \sigma,i\models\psi. $$

Per il prossimo stato:

$$ \sigma,i\models X\varphi $$

se e solo se:

$$ \sigma,i+1\models\varphi. $$

Per until:

$$ \sigma,i\models \varphi U \psi $$

se e solo se esiste una posizione $j\ge i$ tale che:

$$ \sigma,j\models \psi $$

e per ogni $k$ con $i\le k<j$ vale:

$$ \sigma,k\models\varphi. $$

Quindi $U$ e' strong: la seconda formula deve accadere davvero. Ed e' non-strict: puo' accadere gia' nella posizione corrente.

Espansioni fondamentali

Queste equivalenze sono essenziali per tableau e per ragionare oralmente:

$$ F\varphi \equiv \varphi \lor X F\varphi $$

Lettura: prima o poi $\varphi$ vale significa che o vale ora, oppure prima o poi varra' dal prossimo stato.

$$ G\varphi \equiv \varphi \land X G\varphi $$

Lettura: sempre $\varphi$ significa che vale ora e continua a valere sempre dal prossimo stato.

$$ \varphi U \psi \equiv \psi \lor (\varphi\land X(\varphi U \psi)). $$

Lettura: o $\psi$ vale ora, oppure $\varphi$ vale ora e l'obbligo di until viene rimandato al prossimo stato.

3. Varianti di Until e operatori utili

Negli appunti viene sottolineato che esistono piu versioni di until. La versione principale del corso e' strong non-strict.

Strong until

$$ \varphi U \psi $$

richiede che $\psi$ arrivi prima o poi.

Esempio:

$$ busy\;U\;done $$

significa: busy resta vero fino al momento in cui arriva done, e done deve arrivare.

Se done non arriva mai, la formula e' falsa.

Weak until

Il weak until si indica spesso con:

$$ \varphi W \psi. $$

Significa:

$\varphi$ vale fino a $\psi$, ma $\psi$ potrebbe anche non arrivare mai.

Si puo' definire con strong until:

$$ \varphi W \psi := (\varphi U \psi)\lor G\varphi. $$

Esempio:

$$ error\;W\;reset $$

significa: se siamo in errore, restiamo in errore fino al reset; se il reset non arriva mai, l'errore puo' restare per sempre.

Strict until

Nella versione strict, l'evento promesso deve accadere in un futuro proprio, non necessariamente ora.

La differenza si vede su:

$$ p U q. $$

Con until non-strict, se $q$ vale ora, la formula e' gia' vera.

Con until strict, se $q$ vale solo ora e non piu in futuro, la formula non basta.

Release

Un operatore spesso usato nei manuali e':

$$ \varphi R \psi. $$

Si legge "release" ed e' duale di until:

$$ \varphi R \psi := \neg(\neg\varphi U \neg\psi). $$

Intuizione: $\psi$ deve restare vera almeno finche' $\varphi$ non la libera; se $\varphi$ non arriva mai, $\psi$ deve restare vera per sempre.

Non e' indispensabile per il corso, ma aiuta a capire le traduzioni nei tool.

Il pattern "before": $P$ prima di $Q$

Pattern degli appunti, utile negli esercizi: "prima di ogni occorrenza di $Q$ deve esserci un'occorrenza di $P$" ($P\ B\ Q$). Lo scenario da escludere e' "arrivo a $Q$ senza aver mai visto $P$", che e' esattamente $\neg P\ U\ Q$. Quindi:

$$P\ B\ Q \equiv \neg(\neg P\ U\ Q).$$

Tecnica generale: per le proprieta' "negative" spesso conviene scrivere la computazione vietata con un until e negare tutto.

Gli operatori del passato

Si puo' estendere PLTL con gli specchi dei quattro operatori:

Il punto delicato e' lo yesterday nel primo istante: su ℕ lo stato 0 non ha predecessore, quindi $X^- p$ in 0 e' problematica. Si distinguono due varianti:

• debole: "se c'e' un predecessore, li' vale $p$" (vera in 0 — usa l'implicazione $\to$);
• forte: "esiste un predecessore e li' vale $p$" (falsa in 0 — usa la congiunzione $\land$).

Stessa coppia debole/forte gia' vista per l'until: il mnemonico degli appunti e' debole va con $\to$, forte va con $\land$ (sugli interi il problema sparisce, non c'e' un primo istante).

Risultato da ricordare: su tempo lineare discreto il passato non aggiunge potere espressivo a PLTL (ogni formula con passato ha un'equivalente solo futuro), ma aggiunge succintezza: certe proprieta' si scrivono in modo esponenzialmente piu' corto col passato. (Non e' un fatto scontato: in altre logiche temporali il passato aumenta davvero l'espressivita'.)

Il teorema di Kamp e il posto esatto di LTL

L'osservazione chiave degli appunti (p. 228 di notes.pdf): la semantica di ogni operatore LTL e' una formula del primo ordine sulle posizioni —

$$x^i \models p\,U q \iff \exists j\ge i\,\big(x^j\models q \land \forall k\,(i\le k<j \to x^k\models p)\big)$$

usa solo quantificazione su posizioni, l'ordine $<$ e predicati unari (le lettere proposizionali = i $Q_a$ di S1S). Quindi LTL "vive" dentro il frammento del primo ordine di S1S. Kamp dice che lo riempie tutto:

Teorema (Kamp). La teoria monadica del primo ordine degli ordini lineari discreti con primo elemento e' espressivamente equivalente a PLTL (con strong strict until).

Combinato con il capitolo 6 (FO-definibile = star-free), il quadro a tre piani da disegnare all'orale:

$$\text{LTL} \;\equiv\; \text{FO[<]} \;\equiv\; \text{star-free} \;\subsetneq\; \text{ω-regolari} \;\equiv\; \text{S1S} \;\equiv\; \text{Büchi}.$$

Quanto costa decidere LTL

Dagli appunti (rassegna sui tableau):

• soddisfacibilita' di LTL e PLTL: PSPACE-completa;
• frammento con soli $F$/$G$ al posto di $U$ (LTL[F]): NP-completa;
• PLTL su modelli limitati di lunghezza polinomiale: NP-completa;
• il metodo tableau dichiarativo di Wolper (esteso da Lichtenstein-Pnueli al passato) e' esponenziale; esiste un metodo incrementale PSPACE (Kesten et al.).

Distinzioni di classificazione dei metodi (riprese nel Capitolo 8): impliciti vs espliciti (la relazione di accessibilita' e' incorporata nella struttura del tableau vs tracciata con etichette esterne) e dichiarativi vs incrementali (genera tutti i sottoinsiemi di sottoformule e poi elimina, vs genera solo quelli "sensati"). Il corso usa un metodo implicito e dichiarativo (Manna-Pnueli).

4. Pattern LTL da saper tradurre

Questa sezione e' molto importante per l'orale. Se ti danno una frase naturale, devi capire se e' safety, liveness, response, fairness, stabilizzazione, precedenza.

Safety: qualcosa di brutto non accade mai

Frase:

non si entra mai in uno stato bad.

Formula:

$$ G\neg bad. $$

Se esiste un controesempio, lo vedi in un prefisso finito: appena appare bad, la proprieta' e' violata.

Reachability: qualcosa accade prima o poi

Frase:

prima o poi si raggiunge goal.

Formula:

$$ F goal. $$

Response: ogni richiesta viene servita

Frase:

ogni request viene prima o poi seguita da grant.

Formula:

$$ G(request\to F grant). $$

Attenzione: questa formula non dice che il grant corrisponde a quella specifica request in un sistema con molte richieste pendenti; dice solo che dopo ogni posizione con request, in futuro comparira' un grant.

Persistence: da un certo punto in poi sempre

Frase:

prima o poi il sistema diventa stabile e resta stabile.

Formula:

$$ F G stable. $$

Recurrence: infinitamente spesso

Frase:

il processo entra infinitamente spesso in sezione critica.

Formula:

$$ G F critical. $$

Lettura: da ogni posizione futura, esiste ancora piu avanti una posizione in cui vale critical.

Always eventually

Frase:

il sistema torna sempre prima o poi pronto.

Formula:

$$ G F ready. $$

Questo non significa che ready sia sempre vero. Significa che non scompare definitivamente.

Eventually always

Frase:

da un certo punto in poi il sistema e' sempre pronto.

Formula:

$$ F G ready. $$

Differenza fondamentale:

• $GF ready$: ready compare infinite volte;
• $FG ready$: dopo un certo punto ready vale sempre.

Quindi:

$$ FG ready \Rightarrow GF ready $$

ma non viceversa.

Fairness debole

Frase:

se un'azione resta sempre abilitata da un certo punto in poi, allora viene eseguita infinite volte.

Formula:

$$ F G enabled \to G F taken. $$

Questa e' una forma di weak fairness.

Fairness forte

Frase:

se un'azione e' abilitata infinite volte, allora viene eseguita infinite volte.

Formula:

$$ G F enabled \to G F taken. $$

Questa e' una forma di strong fairness.

Precedenza

Frase:

grant non puo' accadere prima di request.

Se voglio dire che non ci sono grant finche' non arriva una request, e request potrebbe anche non arrivare mai, uso weak until:

$$ \neg grant\;W\;request. $$

Senza weak until:

$$ (\neg grant\;U\;request)\lor G\neg grant. $$

Se invece voglio imporre anche che prima o poi arrivi una request, uso strong until:

$$ \neg grant\;U\;request. $$

Stabilizzazione dopo reset

Frase:

se avviene reset, allora dal passo successivo il sistema resta safe.

Formula:

$$ G(reset\to XG safe). $$

Qui $X$ evita di imporre safe nello stesso istante del reset.

5. Valutare formule LTL su una computazione

Considera la computazione:

$$ \sigma=s0,s1,s2,s3,\ldots $$

con labeling:

• in $s0$ vale p;
• in $s1$ vale p;
• in $s2$ vale q;
• da $s3$ in poi vale p a posizioni alterne.

Formula 1: $p U q$

Alla posizione 0:

• $q$ vale in posizione 2;
• $p$ vale nelle posizioni 0 e 1;
• quindi $p U q$ e' vera.

Alla posizione 2:

• $q$ vale subito;
• siccome until e' non-strict, $p U q$ e' vera anche se $p$ non vale in posizione 2.

Formula 2: $G p$

Falsa alla posizione 0, perche' in posizione 2 non vale necessariamente $p$.

Formula 3: $F q$

Vera alla posizione 0, perche' $q$ compare in posizione 2.

Formula 4: $G F p$

Dipende dalla coda. Se da $s3$ in poi $p$ compare a posizioni alterne, allora e' vera: da qualunque punto futuro troverai ancora un punto con $p$.

Formula 5: $F G p$

Falsa se $p$ compare solo a posizioni alterne, perche' non c'e' nessun punto dopo cui $p$ resta sempre vero.

6. LTL e automi di Buchi

Il collegamento centrale e':

a ogni formula LTL si puo' associare un automa di Buchi che riconosce esattamente le tracce che soddisfano la formula.

Questo e' utile per il model checking.

Supponiamo di avere:

• un sistema $S$, visto come generatore di tracce infinite;
• una specifica LTL $\varphi$.

Vogliamo verificare:

$$ Lang(S)\subseteq Lang(\varphi). $$

Equivalentemente:

$$ Lang(S)\cap Lang(\neg\varphi)=\emptyset. $$

Quindi cerchiamo un controesempio:

1. costruiamo l'automa di Buchi per $\neg\varphi$;
2. facciamo il prodotto con il sistema;
3. controlliamo se il prodotto ha un ciclo accettante raggiungibile.

Se il prodotto e' vuoto, non esiste nessuna computazione del sistema che viola $\varphi$.

Se non e' vuoto, una parola accettata e' un controesempio.

Esempio concettuale: response

Formula:

$$ \varphi=G(request\to F grant). $$

Negazione:

$$ \neg\varphi = F(request\land G\neg grant). $$

Lettura:

esiste una posizione in cui compare una request e da quel punto in poi non compare mai grant.

L'automa per la negazione puo' essere pensato cosi':

• stato iniziale: non ho ancora scelto la request cattiva;
• quando vedo request, posso decidere che quella e' la request da controllare;
• da quel momento devo vedere sempre not grant;
• se compare grant, quella scelta fallisce;
• se resto per sempre nella zona senza grant, ho trovato una violazione.

Questa intuizione e' spesso piu importante, all'orale, del disegno completo dell'automa.

7. Tableau LTL: richiamo essenziale

Il tableau LTL serve a decidere la soddisfacibilita' di una formula:

esiste almeno una computazione infinita che soddisfa la formula?

Il punto delicato e' che gli operatori temporali generano promesse future. Una formula come:

$$ F p $$

promette che prima o poi $p$ verra' realizzata.

Una formula come:

$$ p U q $$

promette che prima o poi $q$ verra' realizzata.

Chiusura

Data una formula $\varphi$, la chiusura contiene:

• la formula stessa;
• le sue sottoformule;
• le negazioni;
• le formule next necessarie per espandere $G$, $F$ e $U$.

Esempio:

$$ \varphi=G p\land F\neg p. $$

Le formule rilevanti sono:

• $\varphi$;
• $G p$;
• $F\neg p$;
• $XG p$;
• $XF\neg p$;
• $p$;
• $\neg p$;
• le rispettive negazioni.

Atomi

Un atomo e' un insieme massimale e localmente coerente di formule della chiusura.

Deve rispettare:

• per ogni formula, contiene lei oppure la sua negazione;
• se contiene una congiunzione, contiene entrambi i congiunti;
• se contiene $G p$, contiene $p$ e $XG p$;
• se contiene $F p$, contiene $p$ oppure $XF p$;
• se contiene $p U q$, contiene $q$ oppure contiene $p$ e $X(p U q)$.

Archi del tableau

Metto un arco da un atomo $A$ a un atomo $B$ se le formule next di $A$ sono rispettate in $B$.

Intuizione:

se $A$ dice "nel prossimo stato deve valere p", allora il successore $B$ deve contenere p.

Cammini fulfilling

Un cammino infinito nel tableau e' buono solo se realizza tutte le promesse.

Se lungo il cammino compare infinitamente l'obbligo $F p$, allora il cammino deve contenere punti in cui $p$ viene effettivamente realizzato.

Se un ciclo mantiene per sempre $F p$ ma non visita mai $p$, quel ciclo non e' fulfilling.

Criterio

Una formula LTL e' soddisfacibile se e solo se il tableau contiene un cammino infinito fulfilling che parte da un atomo contenente la formula.

Poiche' il tableau e' finito, la ricerca si riduce a cercare un sottografo fortemente connesso non transiente che soddisfi tutte le promesse.

8. CTL: Computational Tree Logic

Intuizione

CTL interpreta le formule su stati di una struttura ramificata.

Da uno stato possono partire molti cammini:

$$ s\to s1,\quad s\to s2,\quad s\to s3. $$

LTL guarda una singola computazione:

$$ s,s1,\ldots $$

CTL invece permette di dire:

• su tutti i cammini;
• su almeno un cammino.

Per questo CTL e' una logica branching-time.

Quantificatori di cammino

I due quantificatori sono:

• $A$: per tutti i cammini;
• $E$: esiste almeno un cammino.

Esempi:

$$ AF goal $$

significa:

su tutti i cammini, prima o poi si raggiunge goal.

$$ EF goal $$

significa:

esiste almeno un cammino lungo cui prima o poi si raggiunge goal.

Sono molto diverse:

• $AF goal$ e' una garanzia;
• $EF goal$ e' una possibilita'.

Sintassi CTL: formule di stato e formule di cammino

CTL distingue due livelli.

Le formule di stato sono vere o false in uno stato.

Le formule di cammino sono vere o false lungo un cammino.

Regole principali:

1. ogni proposizione atomica e' formula di stato;
2. combinazioni booleane di formule di stato sono formule di stato;
3. se $\psi$ e' formula di cammino, allora $A\psi$ ed $E\psi$ sono formule di stato;
4. se $\varphi$ e $\psi$ sono formule di stato, allora $X\varphi$ e $\varphi U \psi$ sono formule di cammino.

In CTL, gli operatori temporali devono comparire sotto un quantificatore di cammino.

Quindi sono formule CTL:

$$ EX p,\quad AX p,\quad EF p,\quad AF p,\quad EG p,\quad AG p. $$

Sono formule CTL anche:

$$ E[p U q],\quad A[p U q]. $$

Non e' una formula CTL:

$$ X F p. $$

Motivo: in CTL non puoi mettere due operatori temporali di cammino uno dopo l'altro senza reinserire un quantificatore di cammino.

Semantica degli operatori principali

Sia $M=(S,R,L)$ e sia $s\in S$.

EX

$$ M,s\models EX p $$

se esiste un successore $t$ di $s$ tale che:

$$ M,t\models p. $$

AX

$$ M,s\models AX p $$

se tutti i successori $t$ di $s$ soddisfano:

$$ M,t\models p. $$

EF

$$ M,s\models EF p $$

se esiste un cammino da $s$ in cui prima o poi si raggiunge uno stato che soddisfa $p$.

AF

$$ M,s\models AF p $$

se lungo ogni cammino da $s$, prima o poi si raggiunge uno stato che soddisfa $p$.

EG

$$ M,s\models EG p $$

se esiste un cammino infinito da $s$ lungo cui $p$ vale sempre.

AG

$$ M,s\models AG p $$

se lungo tutti i cammini da $s$, in tutti gli stati futuri, vale $p$.

Dualita' utili

Queste equivalenze sono molto utili:

$$ AX p \equiv \neg EX\neg p $$

$$ AG p \equiv \neg EF\neg p $$

$$ AF p \equiv \neg EG\neg p $$

Lettura:

• "tutti i successori soddisfano p" equivale a "non esiste un successore che viola p";
• "sempre p su tutti i cammini" equivale a "non esiste un cammino che raggiunge una violazione";
• "su tutti i cammini prima o poi p" equivale a "non esiste un cammino che evita p per sempre".

9. Pattern CTL da saper tradurre

Possibilita'

Frase:

esiste un modo per arrivare al goal.

Formula:

$$ EF goal. $$

Garanzia inevitabile

Frase:

qualunque cosa accada, prima o poi si arriva al goal.

Formula:

$$ AF goal. $$

Sicurezza globale

Frase:

non si raggiunge mai bad.

Formula:

$$ AG\neg bad. $$

Possibilita' permanente

Frase:

da ogni stato resta possibile raggiungere reset.

Formula:

$$ AG EF reset. $$

Questa e' una formula molto importante: dice che il sistema non perde mai la possibilita' di recuperare.

Esistenza di un comportamento sempre sicuro

Frase:

esiste almeno una computazione che resta sempre safe.

Formula:

$$ EG safe. $$

Reazione garantita su tutti i futuri

Frase:

in ogni stato, se parte una request, allora su tutti i cammini prima o poi arriva grant.

Formula:

$$ AG(request\to AF grant). $$

Reazione possibile

Frase:

in ogni stato, se parte una request, allora esiste almeno un futuro in cui arriva grant.

Formula:

$$ AG(request\to EF grant). $$

Questa e' piu debole della precedente.

Prossimo passo controllato

Frase:

se sono in p, allora esiste un successore in cui p resta vero.

Formula:

$$ AG(p\to EX p). $$

Questa formula non dice che tutti i successori mantengono p, solo che almeno uno lo fa.

10. CTL-star e rapporto con LTL/CTL

CTL-star e' una logica piu generale. Permette di combinare liberamente:

• quantificatori di cammino;
• operatori temporali;
• connettivi booleani sulle formule di cammino.

In CTL non puoi scrivere una formula di cammino come:

$$ G F p. $$

Perche' $G$ e $F$ sono due operatori temporali annidati senza quantificatore intermedio.

In CTL-star invece puoi scrivere:

$$ A G F p. $$

che significa:

su tutti i cammini, p accade infinitamente spesso.

Puoi anche scrivere:

$$ E G F p. $$

che significa:

esiste un cammino lungo cui p accade infinitamente spesso.

Queste formule esprimono in modo naturale proprieta' di fairness e recurrence su cammini.

LTL dentro CTL-star

Una formula LTL come:

$$ G(request\to F grant) $$

diventa in CTL-star:

$$ A G(request\to F grant) $$

se voglio dire che tutti i cammini del sistema soddisfano la proprieta'.

Nel model checking LTL, questo quantificatore universale sui cammini e' spesso implicito:

il sistema soddisfa una formula LTL se tutte le sue computazioni la soddisfano.

CTL dentro CTL-star

Ogni formula CTL e' anche una formula CTL-star. CTL-star elimina la restrizione sintattica di CTL.

Quindi:

$$ CTL \subset CTL^\ast $$

e:

$$ LTL \subset CTL^\ast $$

ma LTL e CTL non sono contenute una nell'altra.

11. LTL vs CTL: perche' sono incomparabili

Questo e' uno dei punti piu probabili all'orale.

Errore comune

Si potrebbe pensare:

CTL ha i quantificatori A/E, quindi e' piu espressiva di LTL.

Non e' corretto.

CTL sa parlare molto bene della struttura ramificata, ma impone una forte disciplina sintattica: ogni operatore temporale deve essere immediatamente legato a un quantificatore di cammino.

LTL sa esprimere bene proprieta' lineari come:

$$ G F p,\quad F G p,\quad G(request\to F grant). $$

CTL sa esprimere bene possibilita' ramificate come:

$$ AG EF p. $$

Una proprieta' CTL non esprimibile in LTL

Formula:

$$ AG EF reset. $$

Lettura:

da ogni stato raggiungibile, resta possibile arrivare a reset.

Questa e' una proprieta' strutturale del grafo: in ogni punto dell'albero delle computazioni deve esistere almeno un ramo buono.

LTL guarda ogni cammino singolarmente. Su un singolo cammino non vede le alternative che non sono state prese. Quindi non puo' dire:

anche se questo cammino non va verso reset, da qui c'era comunque un'altra scelta che avrebbe potuto farlo.

Questa e' informazione branching-time.

Una proprieta' LTL non esprimibile in CTL puro

Formula:

$$ G F p. $$

Lettura:

lungo il cammino, p accade infinitamente spesso.

Nel model checking LTL, detta sul sistema, significa:

su ogni computazione del sistema, p accade infinitamente spesso.

In CTL puro non posso scrivere direttamente:

$$ A G F p. $$

perche' $GFp$ e' una formula di cammino con due operatori temporali annidati.

CTL puo' scrivere formule simili, come:

$$ AG AF p. $$

ma questa non e' la stessa cosa. Dice:

da ogni stato raggiungibile, su tutti i cammini futuri, prima o poi p.

La formula CTL forza una garanzia da ogni stato. LTL invece parla della stessa computazione lineare e impone che p ricompaia infinite volte lungo quella computazione.

Esempio intuitivo del perche' AG EF non e' LTL

Immagina uno stato da cui partono due scelte:

• una scelta porta a un ramo dove reset accade;
• un'altra scelta porta a un ramo dove reset non accade mai.

La formula:

$$ EF reset $$

e' vera nello stato, perche' esiste almeno un ramo buono.

Ma una singola computazione LTL che prende il ramo cattivo non vede piu il ramo buono. Per LTL, quella computazione non contiene reset.

Questa e' la differenza fondamentale:

• CTL valuta possibilita' alternative da uno stesso stato;
• LTL valuta cio' che accade lungo una computazione gia' scelta.

L'argomento rigoroso degli appunti: $AG(p\to EF q)$ vs $G(p\to F q)$

Negli appunti c'e' la costruzione che rende precisa l'intuizione. Il candidato LTL piu' vicino a $AG(p\to EFq)$ e' $G(p\to Fq)$ (letto su tutte le computazioni). Ma non sono equivalenti, e la differenza si vede su questo modello:

costruisci un albero in cui, ogni volta che lungo un ramo incontri una $p$, la $q$ promessa sta su un altro ramo che si dirama li'. Puoi farlo in modo che esistano infiniti cammini, ognuno con un numero finito di occorrenze di $q$ — ma con limite infinito: per ogni $k$ c'e' un cammino con almeno $k$ occorrenze di $q$, pero' nessun cammino ne ha infinite.

Su questo modello $AG(p\to EFq)$ e' vera (da ogni $p$ esiste sempre un ramo con una $q$ futura: cambio ramo ogni volta), mentre "$G(p\to Fq)$ su tutte le computazioni" e' falsa: il cammino che contiene infinite $p$ e continua a "mancare" le $q$ non soddisfa $G(p\to Fq)$, perche' su quel singolo cammino, da un certo punto in poi, le $q$ non arrivano.

Per soddisfare la versione LTL con infinite $p$ sullo stesso cammino servono infinite $q$ sullo stesso cammino; alla versione CTL basta che la $q$ esista da qualche parte, anche cambiando cammino infinite volte. Nessuna formula LTL esprime $AG(p\to EFq)$.

Il verso opposto: fairness fuori da CTL

L'inespressibilita' di $GFp$/$FGp$ in CTL non e' solo un fatto sintattico ("non posso scrivere $A\,GF p$"): nessuna combinazione CTL equivale a quelle proprieta'. La conseguenza pratica segnalata negli appunti:

le condizioni di fairness (justice: $\neg FG(\text{enabled}\land\neg\text{taken})$; compassion: $GF\,\text{enabled}\to GF\,\text{taken}$) si scrivono in LTL ma non in CTL. Chi usa CTL per sistemi fair deve incorporare la fairness nel modello (fair-CTL, vincoli sul modello), non nella formula.

Conclusione da orale: LTL e CTL sono incomparabili — $AG\,EF\,reset$ non si esprime in LTL, $GFp$ non si esprime in CTL. CTL* le contiene entrambe.

Un esempio CTL* commentato (e il ruolo della X)

Dagli appunti:

$$AG(p \to EXFp) \to (p \to EGFp)$$

E' una formula (essenzialmente valida) di CTL — nota $XF$ e $GF$: due operatori di stato annidati senza quantificatore di cammino in mezzo, vietati in CTL. Lettura: se ovunque ogni $p$ ha un successore da cui prima o poi si trova un'altra $p$ ($EXFp$), allora da una $p$ si puo' costruire passo passo un cammino con infinite* $p$ ($EGFp$).

Perche' serve la $X$ in $EXFp$? Con il nostro until non-strict (il presente fa parte del futuro), $EFp$ avrebbe il testimone banale "la $p$ corrente": l'antecedente sarebbe soddisfatto senza muoversi, e non si potrebbe concludere nulla sull'esistenza di infinite $p$. La $X$ forza ogni volta un passo in avanti, e l'unico modo di soddisfare sempre l'antecedente e' avere infinite $p$ sul cammino costruito.

Varianti citate per completezza: PCTL (passato sui cammini), DCTL (successori espliciti sinistro/destro su alberi binari), PDCTL* (entrambi).

12. Esercizi svolti di traduzione LTL

Esercizio 1: ogni richiesta viene prima o poi soddisfatta

Frase:

ogni richiesta viene prima o poi soddisfatta.

Proposizioni:

• req: c'e' una richiesta;
• sat: la richiesta viene soddisfatta.

Formula:

$$ G(req\to F sat). $$

Spiegazione:

• $G$ dice: controlla ogni posizione della computazione;
• se in una posizione vale req, allora da quella posizione in poi deve comparire sat;
• non basta $req\to F sat$, perche' controllerebbe solo la posizione iniziale.

Esercizio 2: errore fino al reset

Frase:

se il sistema entra in errore, resta in errore finche' viene resettato.

Se il reset e' obbligatorio:

$$ G(error\to (error\;U\;reset)). $$

Se il reset potrebbe anche non arrivare:

$$ G(error\to (error\;W\;reset)). $$

Senza weak until:

$$ G(error\to ((error\;U\;reset)\lor G error)). $$

Differenza:

• con strong until, reset deve arrivare;
• con weak until, se reset non arriva, error puo' restare vero per sempre.

Esercizio 3: sezione critica infinite volte

Frase:

il processo entra infinitamente spesso in sezione critica.

Formula:

$$ G F critical. $$

Spiegazione:

Da ogni punto futuro, ci sara' ancora piu avanti un punto con critical. Quindi critical non smette mai definitivamente di comparire.

Esercizio 4: non due grant consecutivi senza request in mezzo

Una forma ragionevole e':

$$ G(grant\to X(\neg grant\;W\;request)). $$

Lettura:

dopo un grant, finche' non compare una request, non deve comparire un altro grant.

Se non si vuole usare weak until:

$$ G(grant\to X((\neg grant\;U\;request)\lor G\neg grant)). $$

Osservazione orale: questa formula controlla la distanza tra grant consecutivi e richiede una request in mezzo. Non dice che ogni request produca un grant; quello e' un altro requisito.

13. Esercizi svolti di traduzione CTL

Esercizio 1: da ogni stato e' possibile raggiungere safe

Frase:

da ogni stato e' possibile raggiungere uno stato safe.

Formula:

$$ AG EF safe. $$

Spiegazione:

• $AG$ visita tutti gli stati raggiungibili in tutti i futuri;
• $EF safe$ dice che da ciascuno di questi stati esiste un cammino verso safe.

Questa e' una proprieta' di recuperabilita', non di garanzia.

Esercizio 2: esiste un cammino che raggiunge goal

Frase:

esiste un cammino lungo cui prima o poi si raggiunge goal.

Formula:

$$ EF goal. $$

Esercizio 3: se parte start, allora inevitabilmente heat

Frase:

su tutti i cammini, se parte start allora prima o poi heat.

Formula:

$$ AG(start\to AF heat). $$

Spiegazione:

Ogni volta che arrivo in uno stato con start, qualunque evoluzione futura deve prima o poi arrivare a heat.

Esercizio 4: reset sempre possibile

Frase:

da ogni stato raggiungibile resta sempre possibile fare reset.

Formula:

$$ AG EF reset. $$

Questa e' simile al primo esercizio, ma con reset.

Punto orale: AG AF reset sarebbe piu forte, perche' direbbe che reset e' inevitabile su tutti i cammini. AG EF reset dice solo che resta disponibile una scelta che porta a reset.

14. Esercizi svolti di semantica

Esercizio: casi di until

Valuta:

$$ p U q $$

alla posizione iniziale.

Caso 1

$q$ vale in $s3$ e $p$ vale in $s0,s1,s2$.

Risposta: vera.

Motivo:

• scelgo $j=3$;
• in $s3$ vale $q$;
• in tutte le posizioni precedenti da 0 a 2 vale $p$.

Caso 2

$q$ non vale mai e $p$ vale sempre.

Risposta: falsa per strong until.

Motivo:

• anche se $p$ vale sempre, l'operatore $U$ richiede che $q$ arrivi;
• se volevo permettere che $q$ non arrivasse mai, dovevo usare weak until:

$$ p W q. $$

Caso 3

$q$ vale gia' in $s0$.

Risposta: vera.

Motivo:

• l'until del corso e' non-strict;
• posso scegliere $j=0$;
• non ci sono posizioni precedenti da controllare.

15. Esercizi svolti su CTL e formule simili

Esercizio 1: distinguere EF e AF

Supponi:

• da $s0$ partono due transizioni: una verso $s1$, una verso $s2$;
• da $s1$ si raggiunge goal;
• da $s2$ si entra in un ciclo senza goal.

Allora:

$$ M,s0\models EF goal $$

perche' esiste il cammino via $s1$.

Ma:

$$ M,s0\not\models AF goal $$

perche' il cammino via $s2$ evita goal per sempre.

Esercizio 2: distinguere EG e AG

Supponi:

• da $s0$ partono due cammini;
• nel primo, safe resta sempre vero;
• nel secondo, prima o poi safe diventa falso.

Allora:

$$ M,s0\models EG safe $$

perche' esiste un cammino sempre safe.

Ma:

$$ M,s0\not\models AG safe $$

perche' non tutti i cammini restano safe.

Esercizio 3: formula CTL valida

Considera:

$$ AG(p\to EX p)\to AG(p\to EG p). $$

Intuizione:

• se in ogni stato con $p$ esiste un successore ancora con $p$;
• allora da ogni stato con $p$ posso costruire, passo dopo passo, un cammino infinito tutto in $p$.

Quindi la conseguenza $EG p$ e' giustificata.

Punto orale: qui si sfrutta il fatto che posso scegliere ogni volta un successore buono. E' una costruzione esistenziale di cammino.

Esercizio 4: perche' AG EF q non equivale a una fairness LTL

Formula CTL:

$$ AG EF q. $$

Dice:

da ogni stato e' possibile raggiungere q.

Non dice:

lungo ogni cammino q compare infinite volte.

Infatti, a ogni stato potrebbe esistere un ramo laterale che raggiunge $q$, mentre il cammino effettivamente seguito evita sempre $q$.

La fairness lineare richiede:

$$ G F q. $$

cioe' q deve ricomparire sulla stessa computazione.

16. Classificare formule: LTL, CTL o CTL-star

Questa e' una domanda tipica per controllare se hai capito la sintassi.

Formula 1

$$ G(request\to F grant) $$

E' LTL.

Come specifica di sistema, si intende spesso universalmente su tutti i cammini.

Formula 2

$$ AG(request\to AF grant) $$

E' CTL.

Ogni operatore temporale e' preceduto dal quantificatore di cammino corretto.

Formula 3

$$ A G F p $$

E' CTL-star, non CTL.

Motivo: dentro il quantificatore $A$ ci sono due operatori temporali annidati, $G$ e $F$.

Formula 4

$$ EX EG p $$

E' CTL.

Lettura:

esiste un successore da cui esiste un cammino sempre p.

Formula 5

$$ E(F p\land G q) $$

E' CTL-star, non CTL.

Motivo: la formula di cammino combina due proprieta' temporali sulla stessa path.

17. Collegamento con model checking

LTL model checking

Domanda:

tutte le computazioni del sistema soddisfano la formula LTL?

Approccio:

1. prendo la negazione della formula;
2. la traduco in automa di Buchi;
3. costruisco il prodotto con il sistema;
4. cerco un ciclo accettante raggiungibile.

Se c'e' un ciclo accettante, esiste un controesempio.

Se non c'e', la proprieta' e' verificata.

CTL model checking

Domanda:

quali stati del sistema soddisfano la formula CTL?

Approccio:

1. calcolo gli insiemi di stati che soddisfano le sottoformule;
2. procedo dal basso verso l'alto;
3. alla fine controllo se lo stato iniziale e' nell'insieme della formula completa.

Per esempio:

$$ EF p $$

si calcola come minimo punto fisso:

$$ Z = p \lor EX Z. $$

In parole:

• parti dagli stati che gia' soddisfano $p$;
• aggiungi gli stati che possono andare in quelli gia' trovati;
• ripeti finche' non cambia piu nulla.

Questo spiega perche' CTL model checking e' piu locale: lavora su insiemi di stati, non su automi di parole infinite.

18. Errori comuni

Confondere F G con G F

$$ FG p $$

vuol dire: prima o poi p resta sempre vero.

$$ GF p $$

vuol dire: p accade infinite volte.

Confondere EF con AF

$$ EF p $$

vuol dire: esiste un cammino verso p.

$$ AF p $$

vuol dire: tutti i cammini arrivano a p.

Scrivere formule CTL non ben formate

In CTL non scrivere:

$$ G F p. $$

Devi usare CTL-star oppure una formula CTL diversa, sapendo che non sempre e' equivalente.

Pensare che AG EF p imponga p sul cammino corrente

No. $AG EF p$ dice che p resta raggiungibile da ogni stato. Il cammino effettivo potrebbe non visitare mai p.

Pensare che LTL veda i rami alternativi

No. LTL vede una path. Se una scelta alternativa non e' presa, LTL non puo' osservarla.

19. Risposta orale pronta: LTL vs CTL

Una risposta compatta da orale potrebbe essere:

LTL e CTL sono due logiche temporali per sistemi reattivi, ma hanno una semantica diversa. LTL e' linear-time: valuta formule su singole computazioni infinite. Gli operatori principali sono X, F, G e U. Una formula come G(req -> F grant) dice che lungo una computazione ogni richiesta viene prima o poi servita. Nel model checking si intende che tutte le computazioni del sistema devono soddisfarla, e infatti si usa spesso la traduzione della negazione in un automa di Buchi per cercare un controesempio.

CTL invece e' branching-time: valuta formule sugli stati di una struttura di Kripke e usa quantificatori di cammino A ed E. Quindi posso distinguere tra AF goal, che dice che tutti i cammini raggiungono goal, ed EF goal, che dice che esiste almeno un cammino verso goal. Questo rende CTL adatta a proprieta' di possibilita' e inevitabilita' su sistemi non deterministici.

Le due logiche sono incomparabili. CTL puo' esprimere proprieta' ramificate come AG EF reset, cioe' da ogni stato resta possibile raggiungere reset, che LTL non puo' esprimere perche' guarda una sola computazione alla volta. LTL invece esprime naturalmente fairness lineari come GF p, cioe' p accade infinitamente spesso sulla stessa computazione; CTL puro non puo' scrivere direttamente A GF p per via della sua restrizione sintattica. CTL-star contiene entrambe e permette di combinare liberamente quantificatori di cammino e operatori temporali.

20. Esercizi aggiuntivi svolti

Esercizio A: formula per mutua esclusione

Frase:

due processi non sono mai contemporaneamente in sezione critica.

Formula LTL:

$$ G\neg(crit1\land crit2). $$

Formula CTL equivalente come safety su tutti i cammini:

$$ AG\neg(crit1\land crit2). $$

Nota: qui LTL e CTL sembrano simili, perche' la proprieta' e' puramente universale e di safety.

Esercizio B: accesso sempre possibile

Frase:

da ogni stato e' possibile che il processo 1 entri in sezione critica.

Formula CTL:

$$ AG EF crit1. $$

Questa non e' la stessa cosa di:

$$ AG AF crit1. $$

La seconda dice che l'ingresso in sezione critica e' inevitabile su tutti i futuri.

Esercizio C: starvation freedom

Frase:

se il processo 1 richiede accesso, prima o poi entra in sezione critica.

Formula LTL:

$$ G(req1\to F crit1). $$

Formula CTL forte:

$$ AG(req1\to AF crit1). $$

Differenza:

• LTL, come specifica di sistema, richiede la proprieta' su ogni computazione completa;
• CTL la esprime localmente su ogni stato e su ogni futuro da quello stato.

Esercizio D: esiste una strategia buona?

Frase:

esiste almeno un comportamento infinito in cui il sistema resta sempre safe e visita goal infinite volte.

In CTL puro non posso scrivere direttamente:

$$ E(G safe\land G F goal). $$

Questa e' una formula CTL-star.

In LTL, lungo un singolo cammino, potrei scrivere:

$$ G safe\land G F goal. $$

Ma LTL non esprime il quantificatore esistenziale sul branching della struttura. Per usarla come proprieta' esistenziale del sistema serve un contesto diverso.

21. Domande da orale

1. Che differenza c'e' tra tempo lineare e tempo ramificato?
2. Che cosa significa $X p$ in LTL?
3. Che cosa significa $p U q$? Che succede se $q$ vale gia' ora?
4. Differenza tra strong until e weak until.
5. Differenza tra $GF p$ e $FG p$.
6. Scrivi una formula LTL per "ogni richiesta viene prima o poi servita".
7. Scrivi una formula LTL per weak fairness e una per strong fairness.
8. Che cosa significa $EF p$ in CTL?
9. Che differenza c'e' tra $EF p$ e $AF p$?
10. Che differenza c'e' tra $EG p$ e $AG p$?
11. Perche' $AG EF p$ non impone che p appaia sul cammino corrente?
12. Perche' LTL e CTL sono incomparabili?
13. Fai un esempio di proprieta' CTL non esprimibile in LTL.
14. Fai un esempio di proprieta' LTL non esprimibile in CTL.
15. Che cosa aggiunge CTL-star?
16. Come si collega LTL agli automi di Buchi?
17. Perche' nel model checking LTL si guarda la negazione della formula?
18. Perche' CTL model checking puo' essere fatto con insiemi di stati?

22. Quiz interattivo

23. Mini-scaletta di ripasso

1. Parti dai sistemi reattivi: computazioni infinite.
2. Definisci Kripke structure e cammino.
3. Spiega LTL: sintassi, semantica, $X$, $F$, $G$, $U$.
4. Fai tre pattern LTL: safety, response, fairness.
5. Spiega $GF$ vs $FG$.
6. Collega LTL agli automi di Buchi e alla ricerca di controesempi.
7. Spiega CTL: path quantifiers $A/E$, formule di stato e di cammino.
8. Fai tre pattern CTL: $EF$, $AF$, $AG EF$.
9. Spiega CTL-star: perche' serve e cosa permette.
10. Chiudi con incomparabilita': esempio CTL non LTL e LTL non CTL.