Έλεγχος μοντέλων: Διαφορά μεταξύ των αναθεωρήσεων

Ο έλεγχος μοντέλων συνληθωςσυνήθως εφαρμόζεται σε σχεδιάσεις υλικού. Όσον αφορά το λογισμικό, λόγω της [[Υπολογισιμότητα|μη-επιλυσιμότητας]], η προσέγγιση αυτή δε μπορεί να είναι αμιγώς αλγοριθμική, στην πράξη μπορεί να αποτύχει ή να μη μπορεί να επαληθεύσει ή να διαψεύσει μια δεδομένη ιδιότητα.

Η δομή συνήθως δίνεται σαν περιγραφή σε πηγαίο κώδικα μιας βιομηχανικής [[γλώσσα περιγραφής υλικού|γλώσσας περιγραφής υλικού]] ή μιας ειδικής γλώσσας. Ένα τέτοιο πρόγραμμα αντιστοιχεί σε μια [[πεπερασμένη μηχανή καταστάσεων]] (finite state machine, FSM), δηλ. έναν [[κατευθυνόμενος γράφος|κατευθυνόμενο γράφο]] που αποτελείται από [[Θεωρία_γράφων|κόμβους (σημεία) και ακμές]]. Σε κάθε κόμβο αντιστοιχεί ένα σύνολο ατομικών προτάσεων που δηλώνουν ποιόποιο στοιχείο της μνήμης είναι κάθε φορά. Οι κόμβοι απεικονίζουν καταστάσεις ενός συστήματος, οι ακμές απεικονίζουν πιθανές μεταβάσεις που μπορεί να αλλάζουν την κατάσταση, ενώ οι ατομικές προτάσεις απεικονίζουν τις βασικές ιδιότητες που ισχύουν σε ένα σημίοσημείο της εκτέλεσης.