Βικιπαίδεια

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

Περιήγηση ιστορικού διαδραστικά
← Προηγούμενη διαφοράΕπόμενη διαφορά →
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
ΟπτικήΚώδικας wiki
μΧωρίς σύνοψη επεξεργασίας
Χωρίς σύνοψη επεξεργασίας
Γραμμή 1:
Η '''δομή Κρίπκε''' ([[αγγλική γλώσσα|Αγγλικά]]: ''Kripke structure'') είναι ένας τύπος μη-ντετερμινιστικής μηχανής πεπερασμένων καταστάσεων που προτάθηκε από τον Σάουλ Κρίπκε το 1963 και χρησιμοποιείται στον [[έλεγχος μοντέλων|έλεγχο μοντέλων]] για να αναπαριστά τη συμπεριφορά ενός συστήματος. Αποτελείται από ένα [[θεωρία γράφων|γράφο]], οι κόμβοι του οποίου αναπαριστούν τις προσβάσιμες καταστάσεις του συστήματος και οι ακμές του τις μεταβάσεις μεταξύ καταστάσεων. Μια συνάρτηση απόδοσης ετικετών (labeling function) ανιτιστοιχεί σε κάθε κόμβο ένα σύνολο από ιδιότητες που ισχύουν σε μια συγκεκριμένη κατάσταση. Οι [[χρονική λογική|χρονικές λογικές]] συνήθως ερμηνεύονται με δομές Κρίπκε.
 
<!--
== Τυπικός ορισμός ==
Έστω ότι το <math>AP</math> beείναι aένα set ofσύνολο ''atomicατομικών [[Propositional calculus|propositions]]προτάσεων'', i.eδηλ. booleanεκφράσεις expressionsαληθείας overμε variablesμεταβλητές, constantsσταθερές andκαι predicateκατηγορηματικά symbolsσύμβολα.
 
AΜια Kripkeδομή structureΚρίπκε<ref>Clarke, Grumberg and Peled: "Model Checking", pageσελ. 14. The MIT Press, 1999.</ref> isείναι aμια [[n-tuple|4-tuple]]τετράδα <math>M = (S,\; I,\; R,\; L)</math> consistingπου ofαποτελείται από:
* aένα [[finiteπεπερασμένο set]]σύνολο of statesκαταστάσεων <math>S\;</math>
* aένα setσύνολο ofαπό initialαρχικές statesκαταστάσεις <math>I \subseteq S</math>
* aμια transitionσχέση relationμετάβασης <math>R \subseteq S \! \times \! S \;</math> whereόπου <math>\; \forall s \! \in \! S, \; \exist s^' \!\! \in \! S</math> suchτέτοιο thatώστε <math> (s,s^') \in R</math>
* aμια labelingσυνάρτηση απόδοσης ετικετών (orή ''interpretationερμηνείας'') function <math>L: S \rightarrow 2^{AP}</math>
 
Επειδή η ''R'' είναι αριστερά-πλήρης (left-total), είναι πάντα πιθανό να κατασκευαστεί ένα άπειρο μονοπάτι μέσω της δομής Κρίπκε. Κατά αυτόν τον τρόπο μια κατάσταση αδιεξόδου (deadlock) έχει μια εξερχόμενη ακμή πίσω στον εαυτό του.
Since ''R'' is [[left-total]], it is always possible to construct an infinite path through the Kripke structure. Thus a [[deadlock]] state has a single outgoing edge back to itself.
 
Η συνάρτηση απόδοσης ετικετών ''L'' ορίζει για κάθε κατάσταση ''s'' &isin; ''S'' το σύνολο ''L''(''s'') όλων των ατομικών προτάσεων που ισχύουν στο ''s''. Σε μια δομή Κρίπκε, η συνάρτηση μετάβασης πρέπει να είναι πλήρης, δηλ. κάθε κατάσταση πρέπει να έχει μια μετάβαση από τον εαυτό της προς μια άλλη κατάσταση.
The labeling function ''L'' defines for each state ''s'' &isin; ''S'' the set ''L''(''s'') of all atomic propositions that are valid in ''s''.
In a Kripke structure, the transition function should be complete, i.e each and every state should have transition away from it.
-->
 
== Δείτε επίσης ==
Ανακτήθηκε από "https://el.wikipedia.org/wiki/Δομή_Κρίπκε"