Logica temporale lineare

Da Wikipedia, l'enciclopedia libera.

La logica temporale lineare o LTL (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 | modifica wikitesto]

La sintassi minima della logica LTL è la seguente:

\varphi := \sim \varphi|\varphi_1 \wedge \varphi_2|p| \varphi_1 U \varphi_2 | \bigcirc \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 | modifica wikitesto]

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 st se e solo esiste t' > 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' > 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 > 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 e' 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 | modifica wikitesto]

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 \and \beta \iff \pi,s_i \models \alpha\  \and \ \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\ge i\ : \ \pi,s_j \models \alpha
  • \pi,s_i \models G\alpha \iff \forall j\ge i\ : \ \pi,s_j \models \alpha
  • \pi,s_i \models \alpha U \beta \iff  \exists j\ge i\ : \ \pi,s_j \models \beta \ \mbox{ e} \ \forall k \ \mbox{tale che} \ i\le k \le j\ : \ \pi,s_k \models \alpha
  • \pi,s_i \models \alpha R \beta \iff  \forall j\ge i\ : \ \pi,s_j \models \beta \ \mbox{ e} \ \exists k \ \mbox{tale che} \ i\le k \le j\ : \ \pi,s_k \models \alpha

Dove \alpha , \beta sono formule booleane.

Proprietà Sintattiche[modifica | modifica wikitesto]

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 ugualianze si può notare come le espressioni temporali possano essere definite utilizzando solo i simboli \neg, \ X, \ U.

Regole[modifica | modifica wikitesto]

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 | modifica wikitesto]

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

Voci correlate[modifica | modifica wikitesto]

Collegamenti esterni[modifica | modifica wikitesto]