Una struttura di Kripke è un tipo di struttura logica ideata 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.
Si tratta di un adattamento della nozione di sistema a transizione di stati usato nell'ambito del model checking per verificare proprietà formali di un sistema.
Definizione Formalmente, una struttura di Kripke è una tupla (, , , , ), dove: , 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 .
Questa struttura è 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 una struttura 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 Logica modale Logica temporale Logica temporale lineare Struttura (logica matematica)
Altri progetti
Categoria:Logica modale