Logo del sito

V&V-Computational Tree Logic (CTL)

Computational Tree Logic (CTL)

Quando abbiamo voluto modellare proprietà temporali sulle computazioni infinite di un sistema, abbiamo introdotto LTL. LTL è una logica che descrive proprietà lungo una singola computazione (sequenza infinita di stati), utilizzando operatori temporali come Next XX), Until (U), Always (G), Eventually (F).

Tuttavia, LTL ha un limite: è in grado di modellare proprietà solo su un singolo percorso alla volta, e non permette di esprimere proprietà che coinvolgano tutti i possibili percorsi che partono da uno stato.

Per superare questo limite, è stata introdotta CTL, che permette di specificare proprietà che valgono su più rami di computazione. CTL estende LTL introducendo i quantificatori $A$ (tutti i percorsi) ed $E$ (esiste almeno un percorso), permettendo di esprimere proprietà globali sul comportamento del sistema.

Sintassi

Definiamo innanzitutto cosa sono:

  • quantificatori di stato
    • Until (U)
    • neXt (X)
  • quantificato di percorso
    • All (A)
    • Exist (E)

Da qui c’è una distinzione da fare sui tipi di formule:

  • Le formule di stato sono valutate in un singolo stato

    • Una formula di stato dice se una proprietà è vera o falsa guardando solo lo stato attuale e le sue possibili evoluzioni future.

    • Esempio:

      $p \to$ “la variabile p è vera in questo stato” $AFwin \to$ “Da questo stato, ogni possibile computazione porta a uno stato in cui win è vero”

  • Le formule di percorso sono valutate lungo un percorso

    • Una formula di percorso specifica come una proprietà evolve lungo una singola computazione (o cammino) nel sistema.

    • Esempio:

      $Fwin \to$”Lungo questo percorso, prima o poi si raggiunge uno stato in cui win è vero”

💡 Ma attenzione: Una formula di percorso non ha senso se non è associata a uno stato di partenza! Se dico solo $Fwin$, non sto specificando da quale stato parte questa computazione, quindi la formula non può essere valutata in modo chiaro in un modello CTL.

Perché aggiungere A o E trasforma una formula di percorso in una formula di stato?

Quando premettiamo A o E a una formula di percorso, stiamo specificando come quella proprietà si comporta a partire da un determinato stato, considerando tutti i possibili cammini o almeno uno di essi.

📌 Esempi concreti:

  1. Formula di percorso (senza stato specificato):

    • $Gsafe \to$ “Sempre, lungo questo percorso, il sistema rimane sicuro.”

      Il problema: Quale percorso? Da dove parte?

  2. Formula di stato (con quantificatore di percorso):

    • $AGsafe \to$ “Da questo stato, ogni possibile computazione porterà sempre a stati sicuri.”

    • $EGsafe \to$ “Da questo stato, esiste almeno una computazione che rimane sempre in stati sicuri.”

      Ora la formula ha senso in un modello!

📌 Differenza chiave:

$Gsafe \to$ Non è una formula valida in CTL, perché manca un riferimento a uno stato iniziale.

$AGsafe \to$ Formula di stato valida, perché possiamo verificarla partendo da uno stato specifico.

💡 Regola generale: Le formule di percorso descrivono proprietà lungo un singolo cammino. Le formule di stato descrivono proprietà valutabili in un singolo stato e includono un quantificatore di percorso per legare la proprietà all’intero sistema.

In generale bisogna ricordare che

  1. $P \in AP \Rightarrow P \text{ formula di stato}$
  2. $p,q \text{ formule di stato } \Rightarrow p\land q, p\lor q, \lnot p \text{ formule di stato}$
  3. $p \text{ formula di percorso}\Rightarrow Ap, Ep \text{ formule di stato}$
  4. $p,q \text{ formule di stato } \Rightarrow pUq, Xp \text{ formule di percorso}$

Strutture

Come in LTL anche in CTL abbiamo delle strutture. In questo caso abbiamo che $M = (S,R,L)$ dove:

  1. S è l’insieme degli stati
  2. $R \subseteq S\times S$
  3. L è la funzione di labeling

Semantica

Per le formule di stato la semantica è la seguente

  • $M,s_0 \vDash P \iff P \in L(s_0)$
  • $M,s_0 \vDash p\land q \iff M,s_0 \vDash p \land M,s_0 \vDash q$
  • $M,s_0 \vDash p\lor q \iff M,s_0 \vDash p \lor M,s_0 \vDash q$
  • $M,s_0 \vDash \lnot p \iff M,s_0 \nvDash p$

  • $M,s_0 \vDash Ep \iff \exists x = (s_0 , \dots) (M,x \vDash p)$

  • $M,s_0 \vDash Ap \iff \forall x = (s_0, \dots) (M,x \vDash p)$

Mentre per le formule di percorso non ci accontentiamo di verificare il singolo stato, ma al contrario dobbiamo considereare tutta la computazione

  • $M,x \vDash P \iff x=(s_0,\dots) \land M,s_0 \vDash p$
  • $M,x \vDash p\land q \iff M,x \vDash p \land M,x\vDash q$
  • $M,x \vDash p\lor q \iff M,x \vDash p \lor M,x \vDash q$
  • $M,x \vDash \lnot p \iff M,x \nvDash p$
  • $M,x \vDash pUq \Rightarrow \exists i(M,x(i)) \vDash q \land \forall j \lt i (M,x(j)\vDash p)$
  • $M,x \vDash Xp \iff M,x(1) \vDash p$

Computational Tree Logic* (CTL*)

CTL* è una variante estesa di CTL che consente di utilizzare più di un simbolo di stato tra due di percorso.

CTL vs LTL

CTL e LTL sono due logiche temporali sostanzialmente differenti e con poteri espressivi diversi. In particolare

  • CTL non è in grado di esprimere vincoli di fairness,
  • LTL non è in grado di esprimere la vincoli di possibilità.