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$.

${\textstyle R}$ è assunta essere totale. Per ogni stato $s$ esiste uno stato ${\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:

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 ${\textstyle \pi =s_{0},s_{1},...\in S^{*}}$ tale che ${\textstyle s_{0}\in I}$ e ${\textstyle (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

Altri progetti

Altri progetti

• Wikimedia Commons

• Wikimedia Commons contiene immagini o altri file su Modelli di Kripke