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 modifica

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 modifica

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 modifica

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 modifica

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 modifica

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 modifica

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