V&V-Linear Temporal Logic

Linear Temporal Logic (LTL)

Ancora una volta introduciamo un modello che serve per rappresentare qualcosa in modo formale, permettendoci di maneggiarne proprietà e risultati.

In questo caso il modello che introduciamo è il modello LTL che serve a rappresentare il tempo, visto come una sequenza di istanti.

Il modello da cui partiremo è il modello PLTL(Propositional Linear Temporal Logic), ma ne esistono di altri tipi che chi è interessato può trovare in fondo all’articolo.

Propositional Linear Temporal Logic

Di seguito introdurrò i mattoncini di base per comprendere questo modello e iniziare a utilizzarlo, per cui introdurrò

• la sintassi di base
• le varie abbreviazioni che si possono usare
• le strutture presenti
• la semantica

Sintassi

La sintassi di PLTL è piuttosto semplice. Abbiamo:

• lettere proposizionali
  • maiuscole: indicano proposizioni
  • minuscole: indicano variabili proposizionali generiche
• connettori logici: $\to, \land, \lor, \lnot$
• connettori temporali:
  • $X$ = neXt = istante immediatamente successivo
    • $Xp$ significa che p è vero nell’istante immediatamente successivo
  • $U$ = Until
    • $p\;Uq$ significa che p è vero almeno fintanto che q non diventa vero
• formule: si formano a partire dalle lettere proposizionali e i congiuntivi temporali e logici

👁️ Attenzione, esistono più versioni di Until

Non esiste solo una versione della proposizione Until, bensì 4:

Abbreviazioni

Per evitare di scrivere formule un sacco lunghe, possiamo usare le abbreviazioni seguenti:

Strutture

In PLTL potremmo vedere la struttura/modello seguente:

In cui:

• S è l’insieme degli stati
• x è una sequenza infinita di stati tale che $x\in S^{\omega}$

• L è la funzione di labeling tale che

Possiamo vedere un modello $M$ come:

• l’insieme degli stati (o configurazioni) di un sistema
• la sequenza infinita di stati x che rappresenta una specifica esecuzione del sistema
• la funzione L che indica quali proprietà sono vere in ogni stato.

Semantica

Se vedete scritte cose tipo

dovete interpretarlo come “$p$ è vero in $M$ all’istante $x(0)$”. Vi potreste chiedere: ma perchè se c’è scritto $x$ noi lo vediamo come $x(0)$? Bè, perchè è una questione di notazione. Ad esempio per indicare “ogni istante di tempo” scriviamo $x^i$

in particolare $x = s_0 = x(0)$

Perciò diremo che $M,x^i \vDash \varphi$ se e solo se:

$M,x^i \vDash P \iff P \in L(s_i)$

$M,x^i \vDash p \land q \iff (M,x^i \vDash p) \land (M,x^i \vDash q) $

$M,x^i \vDash p \lor q \iff (M,x^i \vDash p) \lor (M,x^i \vDash q) $

$M,x^i \vDash \lnot p \iff M,x^i \not \vDash p $

$M,x^i \vDash p U q\iff \exists j \ge i (M,x^j \vDash q) \land \forall i \le k \le j(M,x^i \vDash p)$

$M,x^i \vDash Xp \iff M,x^{i+1} \vDash p$

Teorema di Kamp

Il frammento di prim’ordine di S1S è equivalente a LTL con strict-strong until, perciò LTL ha la stessa potenza espressiva delle espressioni $\omega$-regolari.

Tableau-based decision procedure

La tableau-based decision procedure per la Linear Temporal Logic (LTL) è un metodo automatico per verificare la soddisfacibilità di una formula LTL, ossia determinare se esiste almeno un modello che la rende vera.

Prima di spiegare come funziona la procedura di decisione tableu-based, abbiamo bisogno di introdurre alcuni concetti:

• cos’è la $\varphi$-chiusura su $\varphi$
• cosa si intende per $\varphi$-atomo

$\varphi$-chiusura

A partire da una formula $\varphi$ è possibile definire la sua $\varphi$-chiusura come l’insieme composto da

• $\varphi$ e $\lnot \varphi$
• tutte le sottoformule di $\varphi$
• la negazione di tutti gli elementi dell’insieme
• per tutti i $\psi \in {Gp, Fp, pUq}$ viene aggiunto $X\psi$

Indichiamo questo insieme come $\phi_\varphi$ (si pronuncia “phi di varphi”).

$\varphi$-atomo

Un $\varphi$-atomo lo definisco come un insieme $A$ sottoinsieme di $\phi_\varphi$ che soddisfa queste proprietà:

• non ci devono essere conflitti tra gli elementi di $A$
  • quindi ovviamente solo uno tra $p$ e $\lnot p$ può stare in $A$
• $\forall$ $\alpha$-formula $\in A$ , tutte le scoposizioni $k_\alpha$ devono appartenere ad $A$
• $\forall$ $\beta$-formula $\in A$ , almeno una delle due scoposizioni $k_\beta^{(1)}, k_\beta^{(2)}$ devono appartenere ad $A$

Un qualsiasi sottoinsieme di $\phi_\varphi$ si dice mutualmente soddisfacibile se esiste un modello $\sigma$ e una posizione $j\ge$ 0 tale che ogni elemento dell’insieme vale in posizione $j$ (praticamente è un po’ come dire che un insieme di proprietà è vera all’istante $j$).

Attenzione, non ho detto che il generico sottoinsieme è una $\varphi$-formula, ho solo detto che è un sottoinsieme di $\phi_\varphi$. Difatti per ogni insieme mutualmente soddisfacibile esiste una $\varphi$-formula $A$ tale che $A \subset \phi_\varphi$.

Tableau method

Il metodo dei tableau prevede questi passaggi:

1. ricavo tutti i $\varphi$-atomi e assegno un nodo a ciascuno
2. connetto i nodi A e B se e solo se per ogni $Xp \in \phi_\varphi$ , $Xp \in A$ sse $p \in B$. (quindi essenzialmente guardo $A$ e per ogni formula del tipo $Xp$ cerco il corrispettivo $p$ in $B$)

Perciò seguendo il nostro ragionamento, se $\varphi = Gp \land F\lnot p$ il tableau corrispondente sarà:

Cammino indotto

La definizione formale di cammino indotto è questa:

Dato un modello $\sigma$, il cammino infinito $\pi_\sigma = A_0, A_1, A_2,\dots$ si dice indotto da $\sigma$ se

\[\forall j \ge 0 \land p\in \phi_\varphi \text{ si ha che }(\sigma, j)\Vdash p \iff p\in A_j\]

Sembra complicato, ma vuol dire semplicemente che il cammino $\pi_\sigma$ è indotto se le formule contenute in ogni atomo $A_j$ della successione sono valide nell’istante j-esimo.

Quindi ad esempio se $\pi_\sigma = A_0,A_1,A_2$, allora all’istante $j=0$ tutte le formule di $A_0$ devono essere verificate.

Atomi che realizzano quello che promettono

Quando ho letto sta cosa mi sono immaginato un atomo che è estremamente responsabile e realizza tutto quello che promette. Una sorta di Atomo-Naruto che rispetta il suo credo ninja.

Bè, un atomo $A$ realizza una formula $\psi$ che promette $p$ (tipo $Fp, pUq, \lnot G \lnot p)$ se

• $p \in A$
• $\lnot \psi \in A$

Il secondo punto all’inizio mi sembrava contraddittorio, ma in realtà per come abbiamo definito le cose è corretto. $A$ potrebbe realizzare una formula che non è presente in $A$. Se $\psi$ è in $A$ allora non può esserci $\lnot \psi$ e se non c’è $\psi$ allora può esserci $\lnot \psi$.

Cammino realizzante

Non so voi, ma io più vado avanti con la terminologia tecnica, più sento la testa incasinarsi, quindi inizierò a ragionare più terra-terra, dando meno importanza alla definizione formale e più a quella concettuale.

Ebbene un cammino realizzante è una successione di atomi appartenente al tableau di $\varphi$ in cui per ogni promessa/proprietà futura $\psi \in \phi_\varphi$ si ha che esistono infiniti atomi $A_j$ del cammino, che realizzano tale promessa.

Se volessi scriverlo in gergo tecnico avremmo che:

Un cammino $\pi = A_0,A_1,A_2,\dots \in T_\varphi$ si dice realizzante se per ogni formula $\psi$ che promette $p$ si ha infiniti $A_j$ nel cammino $\pi$ che realizzano $\psi$.

Soddisfacibilità

La formula $\varphi$ è soddisfacibile $\iff T_\varphi$ contiene un cammino realizzante $\pi=A_0,A_1,\dots$ tale che $\varphi \in A_0$

Ma perchè $\varphi \in A_0$? Bè, diciamo che è una garanzia più che una vera necessità. Se non imponessimo che $\varphi$ appartenga al primo atomo del cammino, potremmo considerare un qualsiasi cammino e non per forza quello che verifica la soddisfacibilità di $\varphi$. Se invece

Fulfilling Strongly Connected Subgraph (sottografo fortemente connesso realizzante)

Per SCS si intende un insieme di atomi $S \subset T_\varphi$ per cui vale che per ogni coppia di nodi $(A,B) \in S$ esiste un cammino che li congiunge e composto da soli nodi che appartengono anch’essi a S.

In particolare

Un SCS non-transient $S$ si dice realizzante se $\forall \psi \in \phi_\varphi$ che promette $r$ è realizzata da un atomo in $S$ (ossia $\lnot \psi \in S\;\; \lor \;\; r \in S )$. Un SCS è transient quando è composto da un solo nodo non connesso a sè stesso.

Se riprendiamo il tableau di prima possiamo aiutarci a comprendere meglio il concetto di FSCS.

Ebbene ragioniamo su queste affermazioni:

1. ${A_2, A_3}$ e ${A_5}$ sono FSCS
2. ${A_1}$ e ${A_7}$ non sono FSCS

Dobbiamo ricordarci due cose fondamentali:

1. Se $\varphi = Gp \land F\lnot p$ allora

1. una formula $\psi$ che promette $p$ è del tipo $Fp, pUq, \lnot G \lnot p$. $Gp$ non è una formula che promette qualcosa, perchè dice che p è sempre verificato; non promette che in futuro il suo valore cambierà. Nel nostro insieme $\phi_\varphi$ le formule che promettono sono:

Bè,

• $A_2$ e $A_3$ sono chiaramente fortemente connessi e inoltre
  • per tutte quelle che promettono p sappiamo che la promessa viene mantenuta perchè $p\in A_3$
  • per tutte quelle che promettono $\lnot p$ sappiamo che la promessa viene mantenuta perchè $\lnot p\in A_2$

  perciò S è realizzante.

• $A_5$ è fortemente connesso con sè stesso e inoltre
  • per tutte quelle che promettono p sappiamo che la promessa viene mantenuta perchè $p\in A_3$
  • $\lnot F\lnot p \equiv Gp$ e sappiamo che $p\in A_5$
  • $XF\lnot p$ ma la sua negazione è in $A_5$

  perciò $A_5$ è realizzante

• $A_7$ non è realizzato perchè
  • $F\lnot p$ è presente in $A_7$ quindi non può essere promesso il suo negato (o uno o l’altro possono verificarsi)
• $A_1$ non è realizzato perchè è presente $\lnot F \lnot p$

From LTL to Buchi automata

È possibile far in modo di tradurre un modello LTL in un Buchi automata. Ma perchè dovremmo pensare di farlo? Invece di partire spiegando come fare domandiamoci piuttosto perchè.

Perchè vogliamo tradurre LTL in un automa di Buchi

Quando abbiamo introdotto LTL, abbiamo detto che è un linguaggio efficace per modellare proprietà temporali su successioni infinite di stati. In altri termini, LTL ci permette di descrivere insiemi di computazioni infinite imponendo delle proprietà che devono essere soddisfatte affinché una computazione sia considerata valida.

Il problema principale è che, dato un modello, verificare direttamente se soddisfa una proprietà LTL è computazionalmente difficile. Per questa ragione, utilizziamo gli automi di Büchi, che ci offrono un approccio più strutturato alla verifica.

Gli automi di Büchi:

• Sono progettati per elaborare parole infinite. Se riusciamo a tradurre una formula LTL in un automa di Büchi equivalente, tutte le parole accettate da tale automa rispettano esattamente le proprietà della formula LTL.
• Sono non deterministici, il che ci consente di verificare più possibilità contemporaneamente e di esplorare simultaneamente tutte le possibili computazioni del sistema.
• Sono chiusi rispetto all’intersezione e all’unione, il che ci permette di costruire automi complessi, ad esempio per modellare il comportamento di un sistema e confrontarlo con una specifica.
  • Questo è fondamentale quando costruiamo l’automa prodotto, che rappresenta tutte le computazioni di un modello $M$ che violano la formula $\varphi$.

Traduzione da LTL formula a Buchi automata

Per tradurre da LTL a Buchi automata dobbiamo innanzitutto estendere la semantica di LTL con gli operatori al passato (perciò in realtà la traduzione avviene da LTL+P ad automa).

Gli operatori al passato sono:

• $S$ (since) : “x è stato vero fino a quando y non è diventato vero”

• $Y$ (yesterday) : “vero nell’istante precedente”

• $Z$ (weak Y): “esiste un istante precedente in cui è vero”

• $H$ (history) = $G^-$ : “sempre vero nel passato”

Goal: tradurre $\varphi$ in un automa $\mathcal{A}$ tale che $L(\mathcal{A}_\varphi) = {w \in \mathcal{p}(\Sigma^\omega) | w\vDash \varphi}$

How: trattiamo il tableau come un automa

Quindi: costruiamo l’automa, ma con queste modifiche:

• espandiamo la $\varphi$-chiusura $\phi_\varphi$ imponendo che se $\psi \in {Hp,pSq}$ allora si aggiunge $Yp$ all’insieme $\phi_\varphi$

• espandiamo le regole dei $\varphi$-atomi imponendo che se A è un atomo allora

  • $aSb \in A \iff (b \in A) \lor (a \land a S b \in A)$
  • $Hp \in A \iff (p \land ZHp \in A)$

  Queste due regole bisogna vederle un po’ come le regole che avevamo definito per le $\alpha$-formule e le $\beta$-formule.

A questo punto:

1. STATO INIZIALE DELL’AUTOMA:

   Consideriamo l’atomo che contiene $\varphi$ e nessun $Ya$ o $\lnot Za$

2. TRANSIZIONI

   Corrispondono agli archi dell’automa (circa); $P’ = \delta(P , s)$ (s lettera letta) se:

   • $p \in P \iff p \in S\;\; \forall p \in \Sigma \cap \phi_\varphi$(etichetta dell’arco consistente con lo stato di uscita)
   • $Xa \in P ⟺ p \in P’ \;\;\; \forall Xa \in \phi_\varphi$
   • $Y a \in P’ \iff a \in P \;\;\; \forall Ya \in \phi_\varphi$
   • $Za \in P’ \iff a \in P \;\;\;\forall Za \in \phi_\varphi$

3. STATI FINALI:

   $\forall a \in {p Uq} \cap \phi_\varphi$, lo stato P è $a$-realizzante $\iff$ $a \in P_a \to q \in P$

4. CONDIZIONE DI ACCETTAZIONE:

   Chiaramente l’automa acceta una computazione se e solo se uno stato finale viene raggiunto infinite volte.

LTL+P è più succinto di LTL

📌 Esempio pratico

Consideriamo la proprietà: 📌 “$p$ deve essere sempre vero, tranne forse nel primo istante”

In LTL senza passato:

Questa formula assicura che p sia sempre vero o che diventi sempre vero a partire da un certo punto.

In LTL con il passato:

Questa formula è molto più diretta: dice che p è sempre stato vero ($Hp$) oppure che c’è stato un momento nel passato in cui non lo era ($P\lnot p$).

Dimostrazione:

Passo 1: usiamo LTL+P

Consideriamo la formula “p è vero in uno degli ultimi n istanti”.

Formalmente, in LTL+P possiamo scriverla in modo molto compatto: $\bigvee_{i=0}^{n−1} Y_i p$

Dove:

$Y_ip$ significa “$p$ era vero $i$ istanti fa” (con l’operatore di passato Yesterday Y, che corrisponde all’operatore Next X ma verso il passato).

Questa formula ha lunghezza $O(n)$.

Passo 2: Traduzione in LTL senza passato

In LTL senza passato, non possiamo fare riferimento direttamente al passato, quindi dobbiamo riformulare la condizione usando il futuro. Possiamo esprimere la stessa proprietà dicendo:

Ma questo non è sufficiente, perché dobbiamo poter verificare questa condizione da ogni istante e non solo dall’inizio della parola.

Per farlo, dobbiamo usare una formula più generale che controlli che almeno una delle condizioni precedenti sia stata vera in un prefisso arbitrario della parola. Questo richiede una riscrittura basata su until U:

Questa formula ha lunghezza $O(2^n)$ nel caso peggiore, perché ogni possibile posizione in cui $p$ poteva essere vero in uno degli ultimi $n$ passi richiede una nuova istanza della formula.

Others LTL models

Quantified LTL (QLTL)

• Aggiunge quantificatori sulle lettere proposizionali.

• Permette di esprimere proprietà su insiemi di mondi possibili.
• Le lettere proposizionali possono essere quantificate esistenzialmente ($\exists p$) o universalmente ($\forall p$).

Esempio:

Significa: “per ogni proposizione $p$, se $p$ è vera, rimarrà vera nel prossimo istante”.

📌 Applicazione: Verifica di sistemi con variabili non completamente specificate.

First-Order Linear Temporal Logic (FO-LTL)

• Estende LTL con quantificatori su variabili individuali

• Aggiunge quantificatori ∀x∀x, ∃x∃x e relazioni tra variabili.
• Può esprimere proprietà più complesse rispetto a PLTL.

Esempio:

Significa: “per ogni elemento xx, se ha la proprietà PP, allora anche la sua trasformazione f(x)f(x) la avrà nel prossimo stato”.

📌 Applicazione: Verifica di modelli con strutture dati infinite.

Probabilistic LTL (PLTL o PCTL)*

• Aggiunge operatori probabilistici

• Consente di esprimere la probabilità che un evento si verifichi.
• Si usa nei modelli stocastici.

Esempio:

Significa: “la probabilità che l’evento ‘success’ accada eventualmente è maggiore di 0.9”.

📌 Applicazione: Verifica di sistemi probabilistici, come protocolli di rete o AI.

Metric Temporal Logic (MTL)

• Estende LTL con vincoli temporali espliciti

• Aggiunge intervalli di tempo sugli operatori.

Esempio:

Significa: “$p$ diventerà vero tra 2 e 5 unità di tempo nel futuro”.

📌 Applicazione: Sistemi real-time, controllo industriale.

Linear-Time $\mu$-Calculus

• Aggiunge operatori di “fissaggio di punto” per definire proprietà ricorsive.

• Si usa per descrivere pattern di comportamento infiniti.

Esempio:

Significa: “$p$ sarà vero per sempre o ciclicamente ripetuto”.

📌 Applicazione: Verifica di sistemi con looping o ricorsione.