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:

$\phi :=\mathrm{\top }|p|\mathrm{\neg }\phi |{\phi }_1\wedge {\phi }_2|{\phi }_{1}U{\phi }_2|X\phi$

La sintassi estesa, cioė comprendente gli operatori derivati, aggiunge Eventually ( $\diamond$ ), Globally ( $◻$ ), Precedes, Unless. Questi operatori sono tutti derivabili dall'Until.

Operatori

La logica temporale lineare LTL prevede i seguenti operatori:

• X ($\circ$) , "Next" : $X\phi$ è vera nello stato $s_t$ se e solo se $\phi$ è vera nello stato successivo $s_{t+1}$ ;
• F ($\diamond$) , "Future" (o "Eventually"): $\diamond \phi$ è vera nello stato s_t se e solo esiste $t^{\prime }\ge t$ tale che $\phi$ è vera in $s_{t^{\prime }}$ ;
• G ( $◻$ ) , "Globally" (o "Henceforth"): $◻\phi$ è vera nello stato $s_t$ se e solo se per ogni $t^{\prime }\ge t$ , $\phi$ è vera in $s_{t^{\prime }}$ ;
• U ( $U$ ), "Until": ${\phi }_{1}U{\phi }_2$ è vera in $s_t$ se e solo se $\mathrm{\exists }$ $t_n\ge t$ tale che ${\phi }_2$ è vera in $s_{t_n}$ e $\mathrm{\forall }$ $t_i\in [t,t_{n-1}]$ , ${\phi }_1$ è vera in $s_{t_i}$ ;
• P ( $P$ ) , "Precedes" : ${\phi }_{1}P{\phi }_2$ è vera se non è possibile che esista uno stato futuro in cui vale ${\phi }_2$ preceduto da stati in cui non vale ${\phi }_1$ , questo operatore può essere derivato dall'Until secondo la relazione ${\phi }_{1}P{\phi }_2=\sim (\sim {\phi }_{1}U{\phi }_2)$ ;
• W ( $W$ ), "Unless" : ${\phi }_{1}W{\phi }_2$ è vera se ${\phi }_1$ è vera, a meno che non sia vera ${\phi }_2$ , "Unless" è derivabile secondo la relazione ${\phi }_{1}W{\phi }_2=({\phi }_{1}U{\phi }_2)\vee ◻{\phi }_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à: $\mathrm{\forall }i\in \mathbb{N},(s_i,s_{i+1})\in R$ ;
• $P$ sono le proposizioni atomiche;
• $V:P\times S\to \{true,false\}$ è la funzione di valutazione delle proposizioni atomiche.

La semantica formale degli operatori è così definita:

• $\pi ,s_i\models p\in P\iff V(p,s_i)=true$
• $\pi ,s_i\models \mathrm{\neg }\alpha ⟺\pi ,s_i\models ̸\alpha$
• $\pi ,s_i\models \alpha \wedge \beta ⟺\pi ,s_i\models \alpha \wedge \pi ,s_i\models \beta$
• $\pi ,s_i\models X\alpha ⟺\pi ,s_{i+1}\models \alpha$
• $\pi ,s_i\models F\alpha ⟺\mathrm{\exists }j\ge i:\pi ,s_j\models \alpha$
• $\pi ,s_i\models G\alpha ⟺\mathrm{\forall }j\ge i:\pi ,s_j\models \alpha$
• $\pi ,s_i\models \alpha U\beta ⟺\mathrm{\exists }j\ge i:\pi ,s_j\models \beta \text{ e}\mathrm{\forall }k\text{tale che}i\le k<j:\pi ,s_k\models \alpha$
• $\pi ,s_i\models \alpha R\beta ⟺\mathrm{\forall }j\ge i:\pi ,s_j\models \beta \vee (\mathrm{\exists }l\ge i\text{tale che}\mathrm{\forall }k,i\le k\le 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 ⟺\mathrm{\top }U\alpha$
• $G\alpha ⟺\mathrm{\perp }R\alpha$
• $F\alpha ⟺\mathrm{\neg }G\mathrm{\neg }\alpha$
• $G\alpha ⟺\mathrm{\neg }F\mathrm{\neg }\alpha$
• $\mathrm{\neg }X\alpha ⟺X\mathrm{\neg }\alpha$
• $\alpha R\beta ⟺\mathrm{\neg }(\mathrm{\neg }\alpha U\mathrm{\neg }\beta )$

Da queste uguaglianze si può notare come le espressioni temporali possano essere definite utilizzando solo i simboli $\mathrm{\neg },X,U.$

Regole

Date α e β formule LTL, allora:

• $F\alpha \iff (\alpha \vee XF\alpha )$;
• $G\alpha \iff (\alpha \wedge XG\alpha )$;
• $\alpha \cup \beta \iff (\beta \vee (\alpha \wedge X(\alpha \cup \beta )))$;

Proprietà esprimibili in logica LTL

• Safety: "Non accade mai qualcosa di indesiderato" $◻\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" $◻(request\Rightarrow \diamond reply)$;
• Infinitely Often: "p è vera infinitamente spesso" $◻\diamond p$;
• Fairness: "Se arrivano richieste infinitamente spesso, infinitamente spesso vengono soddisfatte" $◻\diamond request\Rightarrow ◻\diamond reply$;
• Invariant: rappresenta una proprietà (invariante) che il sistema deve sempre mantenere $◻invariant$;
• Eventually Always: "prima o poi arrivo in uno stato dopo il quale vale sempre una proprietà" $\diamond ◻\phi$ .

Voci correlate

• Modelli di Kripke

Collegamenti esterni

• Template:Cita web
• Template:Cita web
• Template:Cita web