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:

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

Operatori[modifica | modifica wikitesto]

La logica temporale lineare LTL prevede i seguenti operatori:

  • X () , "Next" : è vera nello stato se e solo se è vera nello stato successivo  ;
  • F () , "Future" (o "Eventually"): è vera nello stato st se e solo esiste tale che è vera in  ;
  • G ( ) , "Globally" (o "Henceforth"): è vera nello stato se e solo se per ogni , è vera in  ;
  • U ( ), "Until": è vera in se e solo se tale che è vera in e , è vera in  ;
  • P ( ) , "Precedes" : è vera se non è possibile che esista uno stato futuro in cui vale preceduto da stati in cui non vale , questo operatore può essere derivato dall'Until secondo la relazione  ;
  • W ( ), "Unless" : è vera se è vera, a meno che non sia vera , "Unless" è derivabile secondo la relazione .

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 dove:

  • è un insieme infinito di stati;
  • è lo stato iniziale;
  • è la relazione di raggiungibilità:  ;
  • sono le proposizioni atomiche;
  • è la funzione di valutazione delle proposizioni atomiche.

La semantica formale degli operatori è così definita:

Dove sono formule booleane.

Proprietà Sintattiche[modifica | modifica wikitesto]

Date α e β formule LTL, allora:

Da queste ugualianze si può notare come le espressioni temporali possano essere definite utilizzando solo i simboli

Regole[modifica | modifica wikitesto]

Date α e β formule LTL, allora:

  • ;
  • ;
  • ;

Proprietà esprimibili in Logica LTL[modifica | modifica wikitesto]

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

Voci correlate[modifica | modifica wikitesto]

Collegamenti esterni[modifica | modifica wikitesto]