# 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$ .