Modelli di Kripke
# Modelli di Kripke

I modelli di Kripke sono sistemi matematici creati da Saul Kripke per descrivere "sistemi reattivi":

* Sistemi non deterministici con infiniti comportamenti (Protocolli di comunicazione, circuiti hardware, ...);
* Rappresentano l'evoluzione dinamica dei sistemi modellati;
* Uno stato include i valori di variabili di stato, il programma contatori, i contenuti dei canali di comunicazione;
* Possono essere animati e convalidati prima della loro effettiva attuazione.

## Definizione

La definizione formale di un modello di Kripke è rappresentata da ($S$, $I$, $R$, $AP$, $L$), con:

* $S$, insieme degli stati;
* $I$, insieme degli stati iniziali appartenenti all'insieme $S$ degli stati possibili, ovvero $I\subseteq S$;
* $R$, insieme delle possibili transizioni da uno stato $S$ ad un altro stato $S$, ovvero $R\subseteq S\times S$;
* $AP$, insieme delle proposizioni atomiche;
* $L$, funzione di labeling, definita come: $L\subseteq S\times AP$.

R{\textstyle R} è assunta essere totale. Per ogni stato $s$ esiste uno stato $s^′{\textstyle$ s'} tale che $(s,s')\in R$.

Questo modello è rappresentabile graficamente attraverso dei cerchi che rappresentano gli stati e degli archi che li collegano rappresentanti le transizioni. Gli stati possono essere espressi secondo 2 metodi:

* Uno stato identifica univocamente il valore della proposizione atomica che rappresenta;
* Ogni stato può essere etichettato da un vettore di bit (0/1).

Il valore di ogni variabile è sempre assegnato in ogni stato.

Un percorso in un modello di Kripke è rappresentato come una sequenza infinita di stati $π=s_0,$ $s_1,$ $...∈S^∗{\textstyle$ \pi =s_{0}, s_{1}, ...\in S^{*}} tale che $s_0∈I{\textstyle$ s_{0}\in I} e $(s_i,$ $s_{i+1}))∈R{\textstyle$ (s_{i}, s_{i+1}))\in R}.

Uno stato $s$ si dice raggiungibile se esiste un percorso dallo stato iniziale ad esso.

