CTL*

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

Ιστορία

Η LTL έχει προταθεί για την επαλήθευση (verification) προγραμμάτων υπολογιστών από τον Αμίρ Πνουέλι το 1977. Τέσσερα χρόνια αργότερα, το 1981, οι E. M. Κλαρκ και E. A. Έμερσον εφηύραν τη CTL και τον έλεγχο μοντέλων σε CTL. Η CTL* ορίστηκε από τον E. Άλλεν Έμερσον και τον Τζόζεφ Χάλπερν το 1986.

Η CTL και η LTL αναπτύχθηκαν αυτόνομα πριν την CTL*. Και οι δύο λογικές έχουν καταλήξει να είναι πολύ σημαντικές στην κοινότητα του ελέγχου μοντέλων, ενώ η CTL* δεν έχει ακόμα πρακτική σημασία. Παρόλα αυτά, η υπολογιστική πολυπλοκότητα του ελέγχου μοντέλων σε CTL* δεν είναι χειρότερη από αυτήν της LTL: και οι δύο ανήκουν στο PSPACE.

Παραδείγματα τύπων της CTL*

• CTL* τύπος που δεν ανήκει ούτε στην LTL ούτε στη CTL: $EX(p)\land AFG(p)$
• LTL τύπος που δεν ανήκει στη CTL: $\ AFG(p)$
• CTL τύπος που δεν ανήκει στην LTL: $\ EX(p)$
• CTL* τύπος που ανήκει και στη CTL και στην LTL: $\ AG(p)$

Σημείωση: Όταν η LTL θεωρείται υποσύνολο της CTL*, κάθε τύπος της LTL αποκτά έμμεσα ένα πρόθεμα με τον ποσοδείκτη μονοπατιών $\ A$.

Δείτε επίσης

• Δομή Κρίπκε
• Έλεγχος μοντέλων
• Τυπική επαλήθευση
• Χρονική λογική

Αναφορές

• Amir Pnueli: The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46-57. DOI= 10.1109/SFCS.1977.32
• E. Allen Emerson, Joseph Y. Halpern: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33, 1 (Jan. 1986), 151-178. DOI= http://doi.acm.org/10.1145/4904.4999
• Ph. Schnoebelen: The Complexity of Temporal Logic Model Checking. Advances in Modal Logic 2002: 393-436

Εξωτερικοί σύνδεσμοι

• Εκπαιδευτικες διαφάνειες για τη CTL (Αγγλικά)