title: Logica temporale lineare
text: # Logica temporale lineare
  
  La logica temporale lineare o LTL (dall'inglese Linear Temporal Logic) è un'estensione della logica modale nella quale i mondi sono organizzati in una struttura lineare infinita: ogni mondo può così rappresentare un istante di tempo discreto. La logica LTL prevede dunque una organizzazione del tempo lineare, discreta, orientata al futuro e infinita.
  
  Questa logica trova impiego nella analisi dei sistemi i cui modelli possono essere sviluppati secondo le caratteristiche citate, sebbene l'algoritmo di model checking per LTL sia particolarmente complesso e dunque poco utilizzato.
  
  ## Sintassi
  
  La sintassi minima della logica LTL è la seguente:
  
      $\varphi :=\top \ |\ p\ |\ \neg \varphi \ |\ \varphi _{1}\wedge \varphi _{2}\ |\ \varphi _{1}U\varphi _{2}\ |\ X\varphi$
  
  La sintassi estesa, cioė comprendente gli operatori derivati, aggiunge Eventually ( $\diamond$ ), Globally ( $\square$ ), Precedes, Unless. Questi operatori sono tutti derivabili dall'Until.
  
  ## Operatori
  
  La logica temporale lineare LTL prevede i seguenti operatori:
  
  * X ($\circ$) , "Next" : $X\varphi$ è vera nello stato $s_{t}$ se e solo se $\varphi$ è vera nello stato successivo $s_{t+1}$ ;
  * F ($\diamond$) , "Future" (o "Eventually"): $\diamond \varphi$ è vera nello stato $s_t$ se e solo esiste $t'\geq t$ tale che $\varphi$ è vera in $s_{t'}$ ;
  * G ( $\square$ ) , "Globally" (o "Henceforth"): $\square \varphi$ è vera nello stato $s_{t}$ se e solo se per ogni $t'\geq t$ , $\varphi$ è vera in $s_{t'}$ ;
  * U ( $U$ ), "Until": $\varphi _{1}U\varphi _{2}$ è vera in $s_{t}$ se e solo se $\exists$ $t_{n}\geq t$ tale che $\varphi _{2}$ è vera in $s_{t_{n}}$ e $\forall$ $t_{i}\in [t,t_{n-1}]$ , $\varphi _{1}$ è vera in $s_{t_{i}}$ ;
  * P ( $P$ ) , "Precedes" : $\varphi _{1}P\varphi _{2}$ è vera se non è possibile che esista uno stato futuro in cui vale $\varphi _{2}$ preceduto da stati in cui non vale $\varphi _{1}$ , questo operatore può essere derivato dall'Until secondo la relazione $\varphi _{1}P\varphi _{2}=\sim (\sim \varphi _{1}U\varphi _{2})$ ;
  * W ( $W$ ), "Unless" : $\varphi _{1}W\varphi _{2}$ è vera se $\varphi _{1}$ è vera, a meno che non sia vera $\varphi _{2}$ , "Unless" è derivabile secondo la relazione $\varphi _{1}W\varphi _{2}=(\varphi _{1}U\varphi _{2})\vee \square \varphi _{1}$ .
  
  Gli operatori temporali hanno la priorità sugli operatori booleani.
  
  ## Semantica
  
  Per dare la semantica della logica LTL è necessario definire la struttura di interpretazione (modello di Kripke) ossia un modello lineare definito dalla quintupla $\pi =(S,s_{0},R,V,P)$ dove:
  
  * $S$ è un insieme infinito di stati;
  * $s_{0}$ è lo stato iniziale;
  * $R$ è la relazione di raggiungibilità: $\forall i\in \mathbb {N} ,(s_{i},s_{i+1})\in R$ ;
  * $P$ sono le proposizioni atomiche;
  * $V:P\times S\rightarrow \{true,false\}$ è la funzione di valutazione delle proposizioni atomiche.
  
  La semantica formale degli operatori è così definita:
  
  * $\pi ,s_{i}\models p\in P\Leftrightarrow V(p,s_{i})=true$
  * $\pi ,s_{i}\models \neg \alpha \iff \pi ,s_{i}\not \models \alpha$
  * $\pi ,s_{i}\models \alpha \land \beta \iff \pi ,s_{i}\models \alpha \ \land \ \pi ,s_{i}\models \beta$
  * $\pi ,s_{i}\models X\alpha \iff \pi ,s_{i+1}\models \alpha$
  * $\pi ,s_{i}\models F\alpha \iff \exists j\geq i\ :\ \pi ,s_{j}\models \alpha$
  * $\pi ,s_{i}\models G\alpha \iff \forall j\geq i\ :\ \pi ,s_{j}\models \alpha$
  * $\pi ,s_{i}\models \alpha U\beta \iff \exists j\geq i\ :\ \pi ,s_{j}\models \beta \ {\mbox{ e}}\ \forall k\ {\mbox{tale che}}\ i\leq k<j\ :\ \pi ,s_{k}\models \alpha$
  * $\pi ,s_{i}\models \alpha R\beta \iff \forall j\geq i\ :\ \pi ,s_{j}\models \beta \ \vee \ (\exists \ l\geq i\ {\mbox{tale che}}\ \forall k,\ i\leq k\leq l\ :\ \pi ,s_{k}\models \beta \wedge \ \pi ,s_{l}\models \alpha )$
  
  Dove $\alpha ,\beta$ sono formule booleane.
  
  ## Proprietà sintattiche
  
  Date α e β formule LTL, allora:
  
  * $F\alpha \iff \top U\alpha$
  * $G\alpha \iff \bot R\alpha$
  * $F\alpha \iff \neg G\neg \alpha$
  * $G\alpha \iff \neg F\neg \alpha$
  * $\neg X\alpha \iff X\neg \alpha$
  * $\alpha R\beta \iff \neg (\neg \alpha U\neg \beta )$
  
  Da queste uguaglianze si può notare come le espressioni temporali possano essere definite utilizzando solo i simboli $\neg ,\ X,\ U.$
  
  ## Regole
  
  Date α e β formule LTL, allora:
  
  * $F\alpha \Leftrightarrow (\alpha \lor XF\alpha )$;
  * $G\alpha \Leftrightarrow (\alpha \land XG\alpha )$;
  * $\alpha \cup \beta \Leftrightarrow (\beta \lor (\alpha \land X(\alpha \cup \beta )))$;
  
  ## Proprietà esprimibili in logica LTL
  
  * Safety: "Non accade mai qualcosa di indesiderato" $\square \sim bad$;
  * Liveness: "Prima o poi accade qualcosa di desiderato" $\diamond good$;
  * Responsiveness: Un caso particolare di liveness "a fronte di una richiesta prima o poi il sistema risponde" $\square (request\Rightarrow \diamond reply)$;
  * Infinitely Often: "p è vera infinitamente spesso" $\square \diamond p$;
  * Fairness: "Se arrivano richieste infinitamente spesso, infinitamente spesso vengono soddisfatte" $\square \diamond request\Rightarrow \square \diamond reply$;
  * Invariant: rappresenta una proprietà (invariante) che il sistema deve sempre mantenere $\square invariant$;
  * Eventually Always: "prima o poi arrivo in uno stato dopo il quale vale sempre una proprietà" $\diamond \square \varphi$ .
  