MVS - 10 - Model Checking Simbolico I

• Date:

  • [2020-12-16 mer 11:30]

  • [2020-12-21 lun 16:30]

  • [2020-12-23 mer 11:30]

L'idea alla base dei metodi di verifica simbolici è quella di descrivere tramite un linguaggio simbolico gli stati e le transizioni dell'automa da verificare.

Questo approccio alla verifica si differenzia in modo fondamentale da quello visto in precedenza. Il problema del model checking "esplicito", ovvero il model checking in cui si rappresenta esplicitamente l'intero automa con tutti i suoi stati e le sue transizioni è proprio il fatto che il numero di stati tende ad esplodere, e dunque avere una rappresentazione esplicita di tale automa diventa molto velocemente molto costoso.

L'idea del model checking simbolico quindi è quella di rappresentare in modo implicito tanti stati tramite varie formule. Manipolando queste formule si è poi in grado di manipolare tutti gli stati rappresentati da essi, senza doverli esplicitare uno per uno.

Andiamo adesso ad analizzare alcune proprietà generali che una eventuale rappresentazione simoblica deve avere.

Consideriamo le formule di CTL ristretta, ovvero della forma

\[\text{AG}, \text{AF}, \text{EG}, \text{EF}\]

e chiediamoci: che operazioni deve poter supportare la nostra rappresentazione simbolica?

Iniziamo definendo il seguente insieme

\[Sat(\phi) := \text{ insieme degli stati in cui vale } \phi\]

Notiamo che per il modo in cui è stata definita la semantica della CTL possiamo ottenere l'insieme \(Sat(\phi)\) in funzione degli insiemi \(Sat(\psi)\) per ogni sotto-formula \(\psi\) di \(\phi\). In particolare troviamo:

• Se \(\phi\) è una proposizione atomica, allora nella definizione di automa abbiamo ciò che ci serve per costruirci \(Sat(\phi)\). Infatti,

  \[Sat(P) := \{q \in Q: P \in l(q)\}\]

• Se \(\phi\) è ottenuto combinando tra loro sotto formule \(\psi\) con operatori logici, allora possiamo utilizzare la solita associazione tra operatore logico e operatore insiemistico per calcolare il valore di \(Sat(\phi)\). In particolare troviamo,

  \[\begin{split} \phi = \psi_1 \land \psi_2 &\implies Sat(\phi) = Sat(\psi_1) \cap Sat(\psi_2) \\ \phi = \psi_1 \lor \psi_2 &\implies Sat(\phi) = Sat(\psi_1) \cup Sat(\psi_2) \\ \phi = \neg \psi &\implies Sat(\phi) = Q \setminus Sat(\psi) \\ \end{split}\]

• Se invece \(\phi = EX \psi\), allora devo utilizzare la funzione di transizione dell'automa per calcolarmi l'insieme \(Pre(S)\), ovvero l'insieme dei predecessori degli stati in \(S\). In particolare trovo che

  \[Sat(\phi) = Sat(EX \psi) = Pre(Sat(\psi))\]

• Nel caso in cui \(\phi = FX \psi\) non ci basta più \(Pre(S)\) ma dobbiamo calcolare tutti i predecessori a partire dall'insieme \(S\) in modo iterato fino ad arrivare ad un punto fisso. Questo insieme di stati sarà denotato con \(Pre^*(S)\), rappresenta il punto fisso rispetto all'operatore di \(Pre()\), e può essere calcolato con il seguente algoritmo

  X := S
  Y := {}
  
  while X != Y do
        Y := X
        X := X U Pre(X)
  done
  
  return X
  

  Una volta che abbiamo \(Pre^*(S)\) possiamo calcolare \(Sat(\phi)\) nel seguente modo

  \[Sat(\phi) = Sat(FX \psi) = Pre^*(Sat(\psi))\]

• Nel caso in cui \(\phi = AX \psi\) otteniamo

  \[\begin{split} Sat(\phi) = Sat(AX \psi) &= Sat(\neg EX \neg \psi) \\ &= Q \setminus Sat(EX \neg \psi) \\ &= Q \setminus Pre(Sat(\neg \psi)) \\ &= Q \setminus Pre(Q \setminus Sat(\psi)) \\ \end{split}\]

• Nel caso in cui \(\phi = AF \psi\) otteniamo

  \[Sat(\phi) = Sat(AF \psi) = Q \setminus Pre^*(Q \setminus Sat(\psi))\]

• Infine, nel caso in cui \(\phi = A \psi U \psi_2\), abbiamo la seguente riscrittura

  \[A \psi_1 U \psi_2 \equiv \psi_2 \lor \Big(\psi_1 \land (EX \text{ true }) \land AX(A \psi_1 U \psi_2)\Big)\]

  troviamo quindi il seguente algoritmo per il calcolo di \(Sat(\phi)\)

  P1 := Sat(psi_1);
  P2 := Sat(psi_2);
  
  X := P2;
  Y := {};
  
  while (Y != X) {
        Y := X;
        X := X \cup (P1 \cap Pre (Q) \cap (Q \ Pre(Q \ X)));
  }
  
  return X;