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$ è assunta essere totale. Per ogni stato $s$ esiste uno stato $s^{\prime }$ tale che $(s,s^{\prime })\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:

1. Uno stato identifica univocamente il valore della proposizione atomica che rappresenta;
2. 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 $\pi =s_0,s_1,...\in S^{*}$ tale che $s_0\in I$ e $(s_i,s_{i+1}))\in R$.

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

Voci correlate

• Logica temporale lineare