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.

La sintassi minima della logica LTL è la seguente:

${\displaystyle \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 ( ${\displaystyle \diamond }$ ), Globally ( ${\displaystyle \square }$ ), Precedes, Unless. Questi operatori sono tutti derivabili dall'Until.

La logica temporale lineare LTL prevede i seguenti operatori:

• X (${\displaystyle \circ }$) , "Next" : ${\displaystyle X\varphi }$ è vera nello stato ${\displaystyle s_{t}}$ se e solo se ${\displaystyle \varphi }$ è vera nello stato successivo ${\displaystyle s_{t+1}}$ ;
• F (${\displaystyle \diamond }$) , "Future" (o "Eventually"): ${\displaystyle \diamond \varphi }$ è vera nello stato s_t se e solo esiste ${\displaystyle t'\geq t}$ tale che ${\displaystyle \varphi }$ è vera in ${\displaystyle s_{t'}}$ ;
• G ( ${\displaystyle \square }$ ) , "Globally" (o "Henceforth"): ${\displaystyle \square \varphi }$ è vera nello stato ${\displaystyle s_{t}}$ se e solo se per ogni ${\displaystyle t'\geq t}$ , ${\displaystyle \varphi }$ è vera in ${\displaystyle s_{t'}}$ ;
• U ( ${\displaystyle U}$ ), "Until": ${\displaystyle \varphi _{1}U\varphi _{2}}$ è vera in ${\displaystyle s_{t}}$ se e solo se ${\displaystyle \exists }$ ${\displaystyle t_{n}\geq t}$ tale che ${\displaystyle \varphi _{2}}$ è vera in ${\displaystyle s_{t_{n}}}$ e ${\displaystyle \forall }$ ${\displaystyle t_{i}\in [t,t_{n-1}]}$ , ${\displaystyle \varphi _{1}}$ è vera in ${\displaystyle s_{t_{i}}}$ ;
• P ( ${\displaystyle P}$ ) , "Precedes" : ${\displaystyle \varphi _{1}P\varphi _{2}}$ è vera se non è possibile che esista uno stato futuro in cui vale ${\displaystyle \varphi _{2}}$ preceduto da stati in cui non vale ${\displaystyle \varphi _{1}}$ , questo operatore può essere derivato dall'Until secondo la relazione ${\displaystyle \varphi _{1}P\varphi _{2}=\sim (\sim \varphi _{1}U\varphi _{2})}$ ;
• W ( ${\displaystyle W}$ ), "Unless" : ${\displaystyle \varphi _{1}W\varphi _{2}}$ è vera se ${\displaystyle \varphi _{1}}$ è vera, a meno che non sia vera ${\displaystyle \varphi _{2}}$ , "Unless" è derivabile secondo la relazione ${\displaystyle \varphi _{1}W\varphi _{2}=(\varphi _{1}U\varphi _{2})\vee \square \varphi _{1}}$ .

Gli operatori temporali hanno la priorità sugli operatori booleani.

Per dare la semantica della logica LTL è necessario definire la struttura di interpretazione (modello di Kripke) ossia un modello lineare definito dalla quintupla ${\displaystyle \pi =(S,s_{0},R,V,P)}$ dove:

• ${\displaystyle S}$ è un insieme infinito di stati;
• ${\displaystyle s_{0}}$ è lo stato iniziale;
• ${\displaystyle R}$ è la relazione di raggiungibilità: ${\displaystyle \forall i\in \mathbb {N} ,(s_{i},s_{i+1})\in R}$ ;
• ${\displaystyle P}$ sono le proposizioni atomiche;
• ${\displaystyle V:P\times S\rightarrow \{true,false\}}$ è la funzione di valutazione delle proposizioni atomiche.

La semantica formale degli operatori è così definita:

• ${\displaystyle \pi ,s_{i}\models p\in P\Leftrightarrow V(p,s_{i})=true}$
• ${\displaystyle \pi ,s_{i}\models \neg \alpha \iff \pi ,s_{i}\not \models \alpha }$
• ${\displaystyle \pi ,s_{i}\models \alpha \land \beta \iff \pi ,s_{i}\models \alpha \ \land \ \pi ,s_{i}\models \beta }$
• ${\displaystyle \pi ,s_{i}\models X\alpha \iff \pi ,s_{i+1}\models \alpha }$
• ${\displaystyle \pi ,s_{i}\models F\alpha \iff \exists j\geq i\ :\ \pi ,s_{j}\models \alpha }$
• ${\displaystyle \pi ,s_{i}\models G\alpha \iff \forall j\geq i\ :\ \pi ,s_{j}\models \alpha }$
• ${\displaystyle \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 }$
• ${\displaystyle \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 ${\displaystyle \alpha ,\beta }$ sono formule booleane.

Date α e β formule LTL, allora:

• ${\displaystyle F\alpha \iff \top U\alpha }$
• ${\displaystyle G\alpha \iff \bot R\alpha }$
• ${\displaystyle F\alpha \iff \neg G\neg \alpha }$
• ${\displaystyle G\alpha \iff \neg F\neg \alpha }$
• ${\displaystyle \neg X\alpha \iff X\neg \alpha }$
• ${\displaystyle \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 ${\displaystyle \neg ,\ X,\ U.}$

Date α e β formule LTL, allora:

• ${\displaystyle F\alpha \Leftrightarrow (\alpha \lor XF\alpha )}$;
• ${\displaystyle G\alpha \Leftrightarrow (\alpha \land XG\alpha )}$;
• ${\displaystyle \alpha \cup \beta \Leftrightarrow (\beta \lor (\alpha \land X(\alpha \cup \beta )))}$;

• Safety: "Non accade mai qualcosa di indesiderato" ${\displaystyle \square \sim bad}$;
• Liveness: "Prima o poi accade qualcosa di desiderato" ${\displaystyle \diamond good}$;
• Responsiveness: Un caso particolare di liveness "a fronte di una richiesta prima o poi il sistema risponde" ${\displaystyle \square (request\Rightarrow \diamond reply)}$;
• Infinitely Often: "p è vera infinitamente spesso" ${\displaystyle \square \diamond p}$;
• Fairness: "Se arrivano richieste infinitamente spesso, infinitamente spesso vengono soddisfatte" ${\displaystyle \square \diamond request\Rightarrow \square \diamond reply}$;
• Invariant: rappresenta una proprietà (invariante) che il sistema deve sempre mantenere ${\displaystyle \square invariant}$;
• Eventually Always: "prima o poi arrivo in uno stato dopo il quale vale sempre una proprietà" ${\displaystyle \diamond \square \varphi }$ .

• Modelli di Kripke

• Wikimedia Commons contiene immagini o altri file su Logica temporale lineare

• A presentation of LTL (PDF), su dcs.qmul.ac.uk.
• Linear-Time Temporal Logic and Büchi Automata (PDF), su cmi.ac.in.
• Alessandro Artale, LTL Teaching slides (PDF), su inf.unibz.it, Free University of Bozen-Bolzano.

Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica