Λογική υπολογιστικού δένδρου: Διαφορά μεταξύ των αναθεωρήσεων

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