MVS - 05 - Computational Tree Logic
Lecture Info
Date:
In questa lezione abbiamo introdotto il formalismo della computational tree logic, che rappresenta un linguaggio logico adatto a parlare dell'evoluzione di un sistema nel tempo.
1 Summary so Far
1.1 Syncronization
Come abbiamo visto, ci sono tre modi principali per sincronizzare tra loro automi diversi. Questi sono:
Tramite l'invio di messaggi.
Tramite variabili condivise.
Scrivendo la funzione di transizione in un modo specifico.
Quest'ultimo approccio è meno tipico, in quanto l'ingegneria dei sistemi parte dalle componenti, e non dal sistema nella sua intera complessità. In generale infatti è più naturale far comunicare tra loro vari componenti piuttosto che ingegnerizzare direttamente l'intero sistema.
1.2 Verification
La verifica deve passare per il flattering dell'automa iniziale, che viene implicitamente costruito dall'analisi della reachability.
La reachability analysis ci permette di contrastare il fatto che il numero astratto degli stati dell'automa globale è il prodotto del numero degli stati dei vari automi. Questo significa che al crescere delle componenti il numero di stati totali dell'automa globale cresce esponenzialmente. L'ingegnerizzazione di questi sistemi però fa sì che moltissimi potenziali stati non siano mai raggiungibili.
2 The need for Temporal Logic
Fino adesso abbiamo lavorato sul sistema. La verifica però è fatta da due componenti: il sistema e la proprietà del sistema che vogliamo verificare.
Ritornando all'esempio dell'ascensore vogliamo garantire le seguenti proprietà:
Any elevator request must ultimately be satisfied;
The elevator never traverses a floor for which a request is pending without satisfying this request.
Dove per "ultimately" stiamo intendo "prima o poi", ovvero un qualcosa che deve avvenire in un tempo finito ma indeterminato.
Queste proprietà dell'ascensore non fanno riferimento al comportamento statico dell'ascensore, ma bensì a quello dinamico, che fa riferimento all'albero dei cammini di esecuzione.
A questo punto notiamo che nel processo di verifica non possiamo permetterci di utilizzare il linguaggio naturale, in quanto è potenzialmente ambiguo e quindi potrebbe essere molto difficile far capire alla macchina cosa deve verificare.
Un primo approccio potrebbe quindi essere quello di modellare i requisiti utilizzando il linguaggio della logica del primo ordine, e introducendo una variabile temporale \(t\) in modo analogo a quanto viene fatto nella meccanica classica studiata in fisica. Consideriamo ad esempio i seguenti predicati:
\(H(t)\) per indicare che la posizione della cabina al tempo \(t\).
\(\text{app}(n, t)\) per indicare una pending request dal floor \(n\) al tempo \(t\)
\(\text{serv}(n ,t)\) per indicare il floor \(n\) che viene raggiunto dalla cabina al tempo \(t\)
Utilizzando questi predicati possiamo tradurre le richieste di prima nelle seguenti formule
Any elevator request must ultimately be satisfied
\[\forall t, \forall n \Big(\text{app}(n, t) \implies \exists t^{'} > t: \;\; \text{serv}(n, t^{'}) \Big)\]
The elevator never traverses a floor for which a request is pending without satisfying this request.
\[\begin{split} \forall t, \forall t^{'} > t, \forall n \Bigg[\Big(&\text{app}(n, t) \land H(t^{'}) \neq n \land \exists t_{\text{trav}}: \\ & t \leq t_{\text{trav}} \leq t^{'} \land H(t_{\text{trav}}) = n \Big) \\ & \implies \Big( \exists t_{\text{serv}}: t \leq t_{\text{serv}} \leq t^{'} \land \text{serv}(n, t_{\text{serv}} \Big)\Bigg] \end{split}\]
Come è possibile vedere dall'esempio, anche se questo linguaggio potrebbe potenzialmente essere utilizzato per descrivere i nostri requisiti, esso comunque non è ideale. Non sempre infatti le soluzioni del passato sono ideali per i problemi nel presente.
L'idea quindi è quella di creare logiche temporali ad-hoc che sono più semplici della logica del primo ordine e che sono più atte a modellare fenomeni temporali.
3 Computational Tree Logic
La computational tree logic (CTL) è un formalismo logico utilizzato per parlare in modo formale delle proprietà di esecuzione di un dato sistema.
Gli ingredienti della CTL sono i seguenti:
Proposizioni atomiche.
(Classical) boolean combinators
Temporal combinators.
Andiamo adesso a discutere separatamente e in più dettaglio di ciascun aspetto menzioanto. Notiamo in ogni caso che l'ingrediente fondamentale della CTL sono proprio i combinatori temporali, che lavorano al livello dei cammini di esecuzione.
Osservazione: È abbastanza controintuitivo pensare ai singoli cammini di esecuzione, ed è per questo che gli operatori temporali sono stati introdotti solo dopo tanta fatica.
3.1 Atomic propositions
Dato che una esecuzione di un sistema è una sequenza di stati, in CTL ci sono delle proposizioni atomiche che servono per dichiarare proprietà che riguardano i singoli stati. Queste proprietà sono atomiche nel senso che il loro valore di verità è calcolato in funzione del singolo stato su cui vengono dichiarate.
Una proprietà del genere potrebbe essere la proprietà \(\text{nice_weather}\), oppure la proprietà \(\text{open}\). A seconda dello stato in cui mi trovo ciascuna di queste potrebbe essere vera o falsa.
In generale una proprietà atomica \(P\) è vera in uno stato \(q\) se e solo se \(P \in l(q)\), dove \(l(q) \subseteq \text{Prop} = \{P_1, P_2, \ldots \}\) è l'insieme delle proprietà "osservabili" nello stato \(q\).
3.2 Boolean combinators
Oltre alle proprietà atomiche, il nostro linguaggio permette anche l'utilizzo delle classiche costanti booleane true e false e dei classici operatori booleani, tra cui troviamo
\[\begin{split} \neg \;\;\;\; &\longleftrightarrow \;\;\;\; \text{negazione} \\ \land \;\;\;\; &\longleftrightarrow \;\;\;\; \text{congiunzione} \\ \lor \;\;\;\; &\longleftrightarrow \;\;\;\; \text{disgiunzione} \\ \implies \;\;\;\; &\longleftrightarrow \;\;\;\; \text{implicazione logica} \\ \iff \;\;\;\; &\longleftrightarrow \;\;\;\; \text{doppia implicazione} \\ \end{split}\]
Una formula proposizionale è quindi una combinazione tra proposizioni e connettivi booleani. Un esempio di formula proposizione è data da
\[\textbf{error} \implies \neg \textbf{warm}\]
che è vera in tutti gli stati in cui, se vale \(\textbf{error}\), allora non vale \(\textbf{warm}\).
3.3 Temporal combinators
Mentre fino adesso abbiamo parlare dei singoli stati, con l'introduzione degli operatori temporali siamo finalmente in grado di parlare rispetto a determinate sequenze di stati lungo una particolare esecuzione del sistema.
I combinatori temporali più semplici sono tre, e sono:
\[\begin{split} X \;\;\;\; &\longleftrightarrow \;\;\;\; \text{next} \\ F \;\;\;\; &\longleftrightarrow \;\;\;\; \text{future} \\ G \;\;\;\; &\longleftrightarrow \;\;\;\; \text{global} \\ \end{split}\]
3.3.1 Next (X)
L'operatore \(X\) si applica ad una proprietà \(P\) per formare l'espressione ben formata \(X \;\; P\). Tale espressione indica che il prossimo stato del cammino di esecuzione soddisfa \(P\)
Ad esempio se consideriamo l'espressione atomica \(\textbf{warm}\), abbiamo che se \(X \;\; \textbf{warm}\) è vera, allora nel prossimo stato l'espressione atomica \(\textbf{warm}\) è vera.
Per specificare la semantca dell'operatore devo specificare sia il cammino di esecuzione \(\sigma\) che lo stato da cui inizio \(i\). Infatti troviamo la seguente sematica
\[\sigma, i \models X \;\; \phi \iff i < |\sigma| \land \sigma, i + 1 \models \phi\]
Per finire, notiamo le seguenti cose riguardanti l'operatore \(X\):
Può essere applicato a qualsiasi proprietà logica dello stato, come ad esempio \((\textbf{warm} \land \textbf{ok})\).
Può essere applicato a se stesso, per ottenere, ad esempio \(X (X \mathbf{warm})\).
Dato che è possibile avere dei cammini finiti, se ci troviamo alla fine del cammino allora \((X \mathbf{warm})\) diventa falsa.
Riprendendo dall'ultima osservazione, notiamo quindi come l'operatore \(X P\) sta implicitamente chiedendo due cose:
Che il successivo stato esiste;
e che nel successivo stato vale la proprietà \(P\).
3.3.2 Future (F)
\(F \;\; \phi\) invece è vera quando, a partire dallo stato scelto come iniziale, seguendo il cammino scelto, non importa in quanti passi, troviamo uno stato in cui è vera la proprietà \(\phi\).
La semantica di questo operatore è definita come segue
\[\sigma, i \models F \;\; \phi \iff \exists j: \;\; i \leq j \leq |\sigma| \land \sigma, j \models \phi\]
Notiamo come nella definizion futuro del nodo c'è anche il nodo stesso. Il futuro comprende quindi anche il presente. Se voglio il "futuro stretto" posso utilizzare la formula \((X ( F \phi))\).
3.3.3 Globally (G)
\(G \phi\) è vera quando, fissato un certo cammino \(\sigma\) e un punto di partenza su questo cammino \(\sigma_1\), se e solo se in ogni stato del cammino a partire dal punto di partenza scelto vale sempre \(\phi\).
La semantica di questo operatore è definita come segue
\[\sigma, i \models G \;\; \phi \iff \forall j: \;\; i \leq j \leq |\sigma| \land \sigma, j \models \phi\]
3.3.4 Until (U)
\(\phi U \psi\) è vera se, dopo una sequenza finita, eventualmente vuta, in cui vale \(\phi\), vale \(\phi_2\).
Formalmente la semantica di questo operatore è definita come segue
\[\begin{split} \sigma, i \models \phi \;\; U \;\; \psi \iff \exists j: \;\; i \leq j \leq |\sigma|: \;\; &\sigma, j \models \psi \;\; \land \\ &\forall k: i \leq k < j: \sigma, k \models \phi \\ \end{split}\]
3.4 Examples
Consideriamo il seguente esempio
Per fare qualche esempio sulla semantica degli operatori temporali prendiamo qualche cammino dall'esempio del libro
\[\begin{split} \sigma_1 &:= q_0 \to q_1 \to q_0 \to \ldots \\ \sigma_2 &:= q_0 \to q_1 \to q_2 \to q_2 \to \ldots \\ \end{split}\]
Segue quindi qualche esempio sull'operatore \(X\):
Se sono in \(\sigma_1\) e sono in \(q_0\), allora \((X \mathbf{warm})\) non è vera, in quanto il successivo stato è \(q_1\), e in \(q_1\) \(\mathbf{warm}\) è falsa. Se invece considero sempre il cammino \(\sigma_1\) ma lo stato \(q_1\), allora \((X \mathbf{warm})\) è vera.
In \(\sigma_1\) partendo da \(q_0\) abbiamo che \((X (\mathbf{warm} \lor \mathbf{ok}))\) è vera.
In \(\sigma_1\) partendo da \(q_1\) abbiamo che \((X (X \mathbf{warm}))\) è falsa.
Continuando sull'operatore \(F\):
In \(\sigma_1\) partendo da \(q_0\) o anche da \(q_1\) abbiamo che \((F (X \mathbf{warm}))\) è vera.
Continuando sull'operatore \(G\):
In \(\sigma_1\) abbiamo che \((G (\mathbf{ok} \lor \mathbf{error}))\).
Tradurre la seguente frase: "Se la spia dell'olio si accende, allora rimane accesa finché o è sostituito l'olio o la macchina si ferma."
G( If Polio_basso then
Polio_basso U (P_ferma v Psost_olio) )