MVS - 06 - Extended Computational Tree Logic
Lecture Info
Date:
In questa lezione abbiamo esteso il linguaggio logico introdotto nella precedente lezione introducendo i quantificatori temporali che operano sui cammini.
1 Extending CTL
Nella scorsa lezione avevamo visto gli operatori temporali che ci vengono offerti dalla CTL. Tutti questi operatori però operano sulle varie posizioni della stessa execution path.
A partire da uno stato dell'automa però posso costruire l'albero di tutti i cammini possibili, andando ad eseguire ricorsivamente tutte le transizioni valide. Molto spesso l'albero sarà periodico, in quanto ogni volta che ritrovo uno stato l'albero che genero a partire da quello stato è una copia di quello già visto.
Al fine di estendere il nostro linguaggio in modo da poter parlare delle varie possibili esecuzioni a partire da un possibile stato, introduciamo i quantificatori di cammino, che fanno parte della extended computational tree logic e che vengono indicati con i simboli \(A\) (all) ed \(E\) (exists.
1.1 All (A)
Supponiamo di aver scelto un cammino \(\sigma\), e di esserci fermati nell'\(i\) esimo nodo del cammino. A questo punto guardo tutti i cammini che partono dallo stato \(\sigma(i)\).
La proposizione \((A \phi)\) è vera se e solo se \(\phi\) è vera in tutte le possibili continuazioni del cammino \(\sigma\). Il quantificatore A è quindi un quantificatore universale.
Formalmente,
\[\sigma, i \models A \phi \iff \forall \sigma^{'}: \,\, \sigma(0), \ldots ,\sigma(i) = \sigma^{'}(0), \ldots, \sigma^{'}(i): \sigma^{'}, i \models \phi\]
È importante capire la differenza tra \(G\) e \(A\): notiamo infatti che \(G \phi\) ci dice che \(\phi\) è verificata ad ogni passo della singola esecuzione che stiamo considerando, mentre \(A \phi\) ci dice che tutte le esecuzioni possibili arrivate a questo punto soddisfano \(\phi\). In altre parole, l'operatore \(A\) quantifica sui cammini, mentre il quantificatore \(G\) quantifica sulle posizioni di un particolare cammino.
1.2 Exists (E)
Abbiamo poi l'operatore \(E\), che sta per "exists" e che è appunto un operatore esistenziale. Intuitivamente \(E \phi\) è vera se, a partire dallo stato corrente, esiste almeno una execution path che soddisfa \(\phi\).
Formalmente invece troviamo la seguente semantica
\[\sigma, i \models E \phi \iff \exists \sigma^{'}: \,\, \sigma(0), \ldots ,\sigma(i) = \sigma^{'}(0), \ldots, \sigma^{'}(i): \sigma^{'}, i \models \phi\]
2 On the Nature of Time
Passato e futuro non sono computazionalmente equivalenti.
Nell'800 i fisici hanno cominciato a studiare dei fenomeni irriversibili. Consideriamo un mattone caldo. L'esperienza comune che noi abbiamo è che col passare del tempo il mattone diventa sempre più freddo. Nessuno ha però mai visto un mattone che col passare del tempo diventa sempre più caldo. Un assioma della termodinamica dice che il calore passa da un corpo caldo ad uno freddo e non viceversa.
Altri fenomeni fisici invece sono reversibili: leggi di Netwon, rotazione della luna attorno alla terra. Se filmo la luna orbitare attorno alla terra e poi faccio vedere ad una persona il filmato inverso, non è possibile capire se si sta andando avanti o all'indietro. Se invece filmo il lancio una pallina mi accorgo di una differenza, e questa ha a che fare con il fatto che durante lo scontro con il terreno c'è dello scambio di calore derivante dal'attrito.
In generale i fenomeni irreversibili hanno a che fare con la complessità di un sistema.
3 Exercises
Andiamo adesso a tradurre i requisiti che avevamo richiesto alla stampante di qualche lezione fa.
Fairness sulla stampante: se \(a\) chiede di stampare prima o poi stamperà.
\[A G (R_a \implies F(P_a))\]
Notiamo che invece la seguente proprietà non soddisfa la fairness
\[A G (R_a \implies(E(F (P_a))))\]
infatti così facendo garantiamo solo l'esistenza di un cammino che fa stampare \(a\), ma non garantiamo che tutti i cammini fanno stampare \(a\).