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

modifica

La definizione formale di un modello di Kripke è rappresentata da ( ,  ,  ,  ,  ), con:

  •  , insieme degli stati;
  •  , insieme degli stati iniziali appartenenti all'insieme   degli stati possibili, ovvero  ;
  •  , insieme delle possibili transizioni da uno stato   ad un altro stato  , ovvero  ;
  •  , insieme delle proposizioni atomiche;
  •  , funzione di labeling, definita come:  .

  è assunta essere totale. Per ogni stato   esiste uno stato   tale che  .

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   tale che   e  .

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

Voci correlate

modifica

Altri progetti

modifica
  Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica