Δομή Κρίπκε: Διαφορά μεταξύ των αναθεωρήσεων

Η '''δομή Κρίπκε''' ([[αγγλική γλώσσα|Αγγλικά]]: ''Kripke structure'') είναι ένας τύπος μη-ντετερμινιστικής μηχανής πεπερασμένων καταστάσεων που προτάθηκε από τον Σάουλ Κρίπκε το 1963 και χρησιμοποιείται στον [[έλεγχος μοντέλων|έλεγχο μοντέλων]] για να αναπαριστά τη συμπεριφορά ενός συστήματος. Αποτελείται από ένα [[θεωρία γράφων|γράφο]], οι κόμβοι του οποίου αναπαριστούν τις προσβάσιμες καταστάσεις του συστήματος και οι ακμές του τις μεταβάσεις μεταξύ καταστάσεων. Μια συνάρτηση απόδοσης ετικετών (labeling function) ανιτιστοιχείαντιστοιχεί σε κάθε κόμβο ένα σύνολο από ιδιότητες που ισχύουν σε μια συγκεκριμένη κατάσταση. Οι [[χρονική λογική|χρονικές λογικές]] συνήθως ερμηνεύονται με δομές Κρίπκε.