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 }](https://wikimedia.org/api/rest_v1/media/math/render/svg/94a8ad82c18cef4a437ba90be1cf1a3a21a9854b)
La sintassi estesa, cioė comprendente gli operatori derivati, aggiunge Eventually (
), Globally (
), Precedes, Unless. Questi operatori sono tutti derivabili dall'Until.
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.
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:
![{\displaystyle \pi ,s_{i}\models p\in P\Leftrightarrow V(p,s_{i})=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/532e2e1179662bb1decc6946af3aba601eb6d618)
![{\displaystyle \pi ,s_{i}\models \neg \alpha \iff \pi ,s_{i}\not \models \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/167d9f18932666b0d50c2a1b5dfbee1b998d077d)
![{\displaystyle \pi ,s_{i}\models \alpha \land \beta \iff \pi ,s_{i}\models \alpha \ \land \ \pi ,s_{i}\models \beta }](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea5ba33963dc29e6bcac29af6b1b5cd98be96299)
![{\displaystyle \pi ,s_{i}\models X\alpha \iff \pi ,s_{i+1}\models \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/ccb8a27b30337c334dbf962b8d93bcaf26f185ef)
![{\displaystyle \pi ,s_{i}\models F\alpha \iff \exists j\geq i\ :\ \pi ,s_{j}\models \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/5c5eb31b2af6a60c5ce27d468878dcee6f9121b7)
![{\displaystyle \pi ,s_{i}\models G\alpha \iff \forall j\geq i\ :\ \pi ,s_{j}\models \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/6126d60470c3f69c40213a59680c15c29ffa6e7e)
![{\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 }](https://wikimedia.org/api/rest_v1/media/math/render/svg/f441414621c28c231c5ac52b33faaa6c4811bdd0)
![{\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 )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0d362a4ae4b1d1e93f7c0629b54932733f80ae97)
Dove
sono formule booleane.
Date α e β formule LTL, allora:
![{\displaystyle F\alpha \iff \top U\alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/08647faa370044e1269e86ef69c61831a955491d)
![{\displaystyle G\alpha \iff \bot R\alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/e5e6e50671562fc534b750ff03e0a37a746223a6)
![{\displaystyle F\alpha \iff \neg G\neg \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/3bc889cbe708f5258ea57353e61a88c177f41a9a)
![{\displaystyle G\alpha \iff \neg F\neg \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/405815f29062f2506553b9dbfc5980c8ab6b910f)
![{\displaystyle \neg X\alpha \iff X\neg \alpha }](https://wikimedia.org/api/rest_v1/media/math/render/svg/635e038f7b1f033d57e47962d0b32e230c36e8bc)
![{\displaystyle \alpha R\beta \iff \neg (\neg \alpha U\neg \beta )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/48ba891ec82f3a4532e77a2b76d72d0e1eacf833)
Da queste uguaglianze si può notare come le espressioni temporali possano essere definite utilizzando solo i simboli
Date α e β formule LTL, allora:
;
;
;
- 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à"
.