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:
La sintassi estesa, cioė comprendente gli operatori derivati, aggiunge Eventually ( ), Globally ( ), Precedes, Unless. Questi operatori sono tutti derivabili dall'Until.
Operatori 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 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 Date α e β formule LTL, allora:
Da queste uguaglianze si può notare come le espressioni temporali possano essere definite utilizzando solo i simboli
Regole Date α e β formule LTL, allora:
Proprietà esprimibili in logica LTL 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 Logica temporale Struttura di Kripke Computation tree logic
Altri progetti
Collegamenti esterni
Categoria:Logica matematica Categoria:Logica modale Categoria:Logica non classica