Δομή Κρίπκε

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

Τυπικός ορισμός

Έστω ότι το $AP$ είναι ένα σύνολο ατομικών προτάσεων, δηλ. εκφράσεις αληθείας με μεταβλητές, σταθερές και κατηγορηματικά σύμβολα.

Μια δομή Κρίπκε από τρεις καταστάσεις και τις μεταξύ τους μεταβάσεις.

Μια δομή Κρίπκε είναι μια τετράδα $M=(S,\;I,\;R,\;L)$ που αποτελείται από:

• ένα πεπερασμένο σύνολο καταστάσεων $S\;$
• ένα σύνολο από αρχικές καταστάσεις $I\subseteq S$
• μια σχέση μετάβασης $R\subseteq S\!\times \!S\;$ όπου $\;\forall s\!\in \!S,\;\exists s^{'}\!\!\in \!S$ τέτοιο ώστε $(s,s^{'})\in R$
• μια συνάρτηση απόδοσης ετικετών (ή ερμηνείας) $L:S\rightarrow 2^{AP}$

Επειδή η R είναι αριστερά-πλήρης (left-total), είναι πάντα πιθανό να κατασκευαστεί ένα άπειρο μονοπάτι μέσω της δομής Κρίπκε. Κατά αυτόν τον τρόπο μια κατάσταση αδιεξόδου (deadlock) έχει μια εξερχόμενη ακμή πίσω στον εαυτό της.

Η συνάρτηση απόδοσης ετικετών L ορίζει για κάθε κατάσταση s ∈ S το σύνολο L(s) όλων των ατομικών προτάσεων που ισχύουν στο s. Σε μια δομή Κρίπκε, η συνάρτηση μετάβασης πρέπει να είναι πλήρης, δηλ. κάθε κατάσταση πρέπει να έχει μια μετάβαση από τον εαυτό της προς μια άλλη κατάσταση.

Δείτε επίσης

• Χρονική λογική
• Έλεγχος μοντέλων