Modelli di Kripke

Questa voce sull'argomento matematica applicata è solo un abbozzo.

Contribuisci a migliorarla secondo le convenzioni di Teknopedia.

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.

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

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

${\textstyle R}$ è assunta essere totale. Per ogni stato ${\displaystyle s}$ esiste uno stato ${\textstyle s'}$ tale che ${\displaystyle (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 ${\displaystyle s}$ si dice raggiungibile se esiste un percorso dallo stato iniziale ad esso.

• Logica temporale lineare

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

Portale Matematica: accedi alle voci di Teknopedia che trattano di matematica