Λογική υπολογιστικού δένδρου
From Wikipedia, the free encyclopedia
Η λογική υπολογιστικού δένδρου (Computation tree logic, CTL) είναι μια λογική διακλαδιζόμενου χρόνου (branching-time), το οποίο σημαίνει ότι το μοντέλο της για το χρόνο είναι μια δενδρική δομή, στην οποία το μέλλον δεν έχει οριστεί αλλά υπάρχουν διαφορετικά μονοπάτια σε αυτό και κάθε ένα από αυτά τα μονοπάτια μπορεί να είναι ένα μονοπάτι που θα πραγματοποιηθεί. Χρησιμοποιείται στην τυπική επαλήθευση λογισμικού ή υλικού, συνήθως από λογισμικό που ονομάζεται ελεγκτής μοντέλων. Το λογισμικό αυτό προσδιορίζει αν το λογισμικό ή το υλικό που ελέγχεται έχει κάποιες συγκεκριμένες ιδιότητες ασφάλειας (safety) ή ζωτικότητας (liveness). Ανήκει στην κατηγορία των χρονικών λογικών, όπως και η γραμμική χρονική λογική.
![]() |
Το λήμμα παραθέτει τις πηγές του αόριστα, χωρίς παραπομπές. |