Λογική υπολογιστικού δένδρου

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

## Σύνταξη της CTL
Η γλώσσα ενός καλώς ορισμένου τύπου σε CTL παράγεται από την ακόλουθη γραμματική χωρίς συμφραζόμενα:

:\phi::=\bot |\top |p|(\neg\phi)|(\phi\land\phi)|(\phi\lor\phi)|
(\phi\Rightarrow\phi)|(\phi\Leftrightarrow\phi)|AX\phi|EX\phi|AF\phi|EF\phi|AG\phi|EG\phi|
A[\phi U \phi]|E[\phi U \phi]

όπου ο p παίρνει τιμές στο σύνολο των ατομικών τύπων (atomic formulas). Δε χρειάζονται όλοι οι σύνδεσμοι - για παράδειγμα οι 
\{\neg, \land, AX, AU, EU\} αποτελούν πλήρες σύνολο συνδέσμων, με τους υπόλοιπους να μπορούν να οριστούν με βάση αυτούς.

* A σημαίνει 'σε όλα τα μονοπάτια' ('along All paths') ή *Αναπόφευκτα* *(Inevitably)*
* E σημαίνει 'σε ένα τουλάχιστον μονοπάτι' ('along at least - there Exists - one path') ή *Πιθανόν* *(possibly)*

Για παράδειγμα, ο εξής τύπος είναι ένας καλώς ορισμένος τύπος της CTL:

:EF EG p \Rightarrow AF r 

Ο παρακάτω δεν είναι καλώς ορισμένος τύπος της CTL:

:EF \big(r U q\big) 

Το πρόβλημα με αυτόν είναι ότι ο U μπορεί να εμφανίζεται μόνο μαζί με έναν A ή έναν E. Σαν κατασκευαστικά στοιχεία χρησιμοποιεί ατομικές προτάσεις για να δηλώσει ιδιότητες των καταστάσεων ενός συστήματος. Η CTL στη συνέχεια συνδυάζει αυτές τις προτάσεις σε τύπους χρησιμοποιώντας λογικούς τελεστές και χρονικές λογικές.

## Τελεστές

thumb|200px|Ένα μοντέλο της λογικής υπολογιστικού δένδρου

### Λογικοί τελεστές
Οι λογικοί τελεστές είναι οι συνήθεις: \neg,\lor,\land,\Rightarrow και \Leftrightarrow. Οι τύποι της CTL μπορούν επιπλέον να χρησιμοποιούν με αυτούς τις λογικές σταθερές true (αληθές) και false (ψευδές).

### Χρονικοί τελεστές
Οι χρονικοί τελεστές είναι οι ακόλουθοι:
* Ποσοδείκτες πάνω σε μονοπάτια
** **A** \phi - Όλα (**A**ll): η \phi πρέπει να ισχύει σε όλα τα μονοπάτια που αρχίζουν από την τρέχουσα κατάσταση.
** **E** \phi - Υπάρχει (**E**xists): υπάρχει τουλάχιστον ένα μονοπάτι που αρχίζει από την τρέχουσα κατάσταση, στο οποίο να ισχύει η \phi.
* Ποσοδείκτες σε συγκεκριμένα μονοπάτια
** **X** \phi - Επόμενο (Ne**x**t): η \phi πρέπει να ισχύει στην επόμενη κατάσταση (ο τελεστής αυτός συνήθως συμβολίζεται και σαν **N** αντί για **X**).
** **G** \phi - Καθολικά (**G**lobally): η \phi πρέπει να ισχύει σε όλο το υπόλοιπο μονοπάτι.
** **F** \phi - Τελικά (**F**inally): η \phi πρέπει να ισχύει τελικά (κάπου στο υπόλοιπο μονοπάτι).
** \phi **U** \psi - Μέχρι (**U**ntil): η \phi πρέπει να ισχύει *τουλάχιστον* μέχρι κάποια θέση στην οποία να ισχύει η \psi. Αυτό σημαίνει ότι η \psi θα επαληθευτεί στο μέλλον.
** \phi **W** \psi - Ασθενές μέχρι (**W**eak until): η \phi πρέπει να ισχύει μέχρι να ισχύει η \psi. Η διαφορά με τον **U** είναι ότι δεν εξασφαλίζεται ότι η \psi θα επαληθευτεί ποτέ. Ο τελεστής **W** κάποιες φορές αποκαλείται και "εκτός αν" ("unless").

Στη CTL*, οι χρονικοί τελεστές μπορούν να αναμιγνύονται ελεύθερα. Στη CTL, ο τελεστής πρέπει πάντα να ομαδοποιείται σε δύο θέσεις: ένας τελεστής μονοπατιού που ακολουθείται από έναν τελεστή κατάστασης. Δείτε τα παραδείγματα παρακάτω. Η CTL* είναι γνήσια πιο εκφραστική από τη CTL.

### Ελάχιστο σύνολο τελεστών
Στη CTL υπάρχει ένα ελάχιστο σύνολο από τελεστές. Όλοι οι τύποι της CTL μπορούν να μετασχηματιστούν ώστε να χρησιμοποιούν μόνο αυτούς τους τελεστές, κάτι που είναι χρήσιμο στον έλεγχο μοντέλων. Ένα ελάχιστο σύνολο από τελεστές είναι: {false, \lor, \neg, **EG**, **EU**, **EX**}.

Ακολουθούν μερικοί από τους μετασχηματισμούς χρονικών τελεστών:
***EF**\phi == **E**[true**U**(\phi)]   ( επειδή **F**\phi == [true**U**(\phi)] )
***AX**\phi == \neg**EX**(\neg\phi)
***AG**\phi == \neg**EF**(\neg\phi) == \neg **E**[true**U**(\neg\phi)]
***AF**\phi == **A**[true**U**\phi] == \neg**EG**(\neg\phi)
***A**[\phi**U**\psi] == \neg( **E**[(\neg\psi)**U**\neg(\phi\lor\psi)] \lor **EG**(\neg\psi) )

## Σημασιολογία της CTL
### Ορισμός
Οι τύποι της CTL ερμηνεύονται με συστήματα μεταβάσεων (Transition Systems), όπως περιγράφεται τυπικά παρακάτω.

Έστω ότι \mathcal{M}=(S,\rightarrow,L) είναι ένα μοντέλο για τη CTL
:with s \in S, \phi \in F όπου F είναι το σύνολο των καλώς ορισμένων τύπων στην κανονική γλώσσα \mathcal{M}.

Τότε η σημασιολογική σχέση (\mathcal{M}, s \models \phi) ορίζεται από δομική επαγωγή (Structural Induction) στην \phi:
# \Big( (\mathcal{M}, s) \models \top \Big) \Leftrightarrow \Big( (\mathcal{M}, s) \not\models \bot \Big)
# \Big( (\mathcal{M}, s) \models p \Big) \Leftrightarrow \Big( p \in L(s) \Big)
# \Big( (\mathcal{M}, s) \models \neg\phi \Big) \Leftrightarrow \Big( (\mathcal{M}, s) \not\models \phi \Big)
# \Big( (\mathcal{M}, s) \models \phi_1 \land \phi_2 \Big) \Leftrightarrow \Big( \big((\mathcal{M}, s) \models \phi_1 \big) \land \big((\mathcal{M}, s) \models \phi_2 \big) \Big)
# \Big( (\mathcal{M}, s) \models \phi_1 \lor \phi_2 \Big) \Leftrightarrow \Big( \big((\mathcal{M}, s) \models \phi_1 \big) \lor \big((\mathcal{M}, s) \models \phi_2 \big) \Big)
# \Big( (\mathcal{M}, s) \models \phi_1 \Rightarrow \phi_2 \Big) \Leftrightarrow \Big( \big((\mathcal{M}, s) \not\models \phi_1 \big) \lor \big((\mathcal{M}, s) \models \phi_2 \big) \Big)
# \bigg( (\mathcal{M}, s) \models \phi_1 \Leftrightarrow \phi_2 \bigg) \Leftrightarrow \bigg( \Big( \big((\mathcal{M}, s) \models \phi_1 \big) \land \big((\mathcal{M}, s) \models \phi_2 \big) \Big) \lor \Big( \neg \big((\mathcal{M}, s) \models \phi_1 \big) \land \neg \big((\mathcal{M}, s) \models \phi_2 \big) \Big) \bigg)
# \Big( (\mathcal{M}, s) \models AX\phi \Big) \Leftrightarrow \Big( \forall \langle s \rightarrow s_1 \rangle \big( (\mathcal{M}, s_1) \models \phi \big) \Big)
# \Big( (\mathcal{M}, s) \models EX\phi \Big) \Leftrightarrow \Big( \exists \langle s \rightarrow s_1 \rangle \big( (\mathcal{M}, s_1) \models \phi \big) \Big)
# \Big( (\mathcal{M}, s) \models AG\phi \Big) \Leftrightarrow \Big( \forall \langle s_1 \rightarrow s_2 \rightarrow \ldots \rangle (s=s_1) \forall i \big( (\mathcal{M}, s_i) \models \phi \big) \Big)
# \Big( (\mathcal{M}, s) \models EG\phi \Big) \Leftrightarrow \Big( \exists \langle s_1 \rightarrow s_2 \rightarrow \ldots \rangle (s=s_1) \forall i \big( (\mathcal{M}, s_i) \models \phi \big) \Big)
# \Big( (\mathcal{M}, s) \models AF\phi \Big) \Leftrightarrow \Big( \forall \langle s_1 \rightarrow s_2 \rightarrow \ldots \rangle (s=s_1) \exists i \big( (\mathcal{M}, s_i) \models \phi \big) \Big)
# \Big( (\mathcal{M}, s) \models EF\phi \Big) \Leftrightarrow \Big( \exists \langle s_1 \rightarrow s_2 \rightarrow \ldots \rangle (s=s_1) \exists i \big( (\mathcal{M}, s_i) \models \phi \big) \Big)
# \bigg( (\mathcal{M}, s) \models A[\phi_1 U \phi_2] \bigg) \Leftrightarrow \bigg( \forall \langle s_1 \rightarrow s_2 \rightarrow \ldots \rangle (s=s_1) \exists i \Big( \big( (\mathcal{M}, s_i) \models \phi_2 \big) \land \big( \forall (j 
# \bigg( (\mathcal{M}, s) \models E[\phi_1 U \phi_2] \bigg) \Leftrightarrow \bigg( \exists \langle s_1 \rightarrow s_2 \rightarrow \ldots \rangle (s=s_1) \exists i \Big( \big( (\mathcal{M}, s_i) \models \phi_2 \big) \land \big( \forall (j 

### Χαρακτηρισμός της CTL
Οι κανόνες 10-15 παραπάνω αναφέρονται σε υπολογιστικά μονοπάτια σε μοντέλα και είναι αυτοί που τελικά χαρακτηρίζουν το "Υπολογιστικό Δένδρο", είναι βεβαιώσεις σχετικά με τη φύση του υπολογιστικού δένδρου με άπειρο βάθος και ρίζα τη δεδομένη κατάσταση s.

### Σημασιολογική ισοδυναμία
Οι τύποι της CTL \phi και \psi λέγονται σημασιολογικά ισοδύναμοι αν κάθε κατάσταση σε κάθε μοντέλο που ικανοποιεί τον ένα, ικανοποιεί και τον άλλο.
:Αυτό δηλώνεται \phi \equiv \psi

Φαίνεται ότι οι A και E είναι δυικοί (δηλαδή ο ένας μπορεί να οριστεί με βάση τον άλλο), όπως και οι G και F, εφόσον είναι ο καθολικός και ο υπαρξιακός ποσοδείκτης αντίστοιχα στα υπολογιστικά δένδρα.

Οι νόμοι του Ντε Μόργκαν μπορούν να τυποποιηθούν στη CTL όπως στο παρακάτω παράδειγμα:
:\neg AF\phi \equiv EG\neg\phi
:\neg EF\phi \equiv AG\neg\phi
:\neg AX\phi \equiv EX\neg\phi

Από αυτά τα δεδομένα προκύπτει ότι:
:AF\phi \equiv A[\top U \phi]
:EF\phi \equiv E[\top U \phi]

Στην πραγματικότητα, μπορεί να δειχθεί, με τη χρήση αυτών των ταυτοτήτων, ότι ένα υποσύνολο των χρονικών συνδέσμων της CTL αρκεί αν περιέχει τον EU, τουλάχιστον έναν από τους \{AX,EX\} και τουλάχιστον έναν από τους \{EG,AF,AU\}.

Κάποιες επιπλέον σημαντικές ταυτότητες:
:AG\phi \equiv \phi \land AX AG \phi
:EG\phi \equiv \phi \land EX EG \phi
:AF\phi \equiv \phi \lor AX AF \phi
:EF\phi \equiv \phi \lor EX EF \phi
:A[\phi U \psi] \equiv \psi \lor (\phi \land AX A [\phi U \psi])
:E[\phi U \psi] \equiv \psi \lor (\phi \land EX E [\phi U \psi])

## Παραδείγματα
Έστω ότι "P" σημαίνει "μου αρέσει η σοκολάτα" και Q σημαίνει "έχει ζέστη έξω."

***AG**.P
:"Θα μου αρέσει η σοκολάτα από τώρα, ό,τι και να γίνει."
***EF**.P
:"Μπορεί να μου αρέσει η σοκολάτα κάποια μέρα, τουλάχιστον για μία μέρα."
***AF**.**EG**.P
:"Είναι πάντα πιθανό (AF) ότι ξαφνικά θα αρχίσει να μου αρέσει η σοκολάτα για όλον τον υπόλοιπο χρόνο." (Σημείωση: όχι μόνο για την υπόλοιπη ζωή μου, επειδή αυτή είναι πεπερασμένη, ενώ ο **G** είναι άπειρος).
***EG**.**AF**.P
:"Αυτή είναι μια σημαντική στιγμή στη ζωή μου. Ανάλογα με το τι θα συμβεί στη συνέχεια (E), είναι πιθανό ότι για όλον τον υπόλοιπο χρόνο (G), θα υπάρχει πάντα κάποια στιγμή στο μέλλον (AF) που θα μου αρέσει η σοκολάτα. Όμως, αν συμβεί κάτι λάθος την επόμενη στιγμή, δεν γνωρίζω αν θα μου αρέσει ποτέ η σοκολάτα."
***A**(P**U**Q)
:"Από τώρα και μέχρι να έχει ζέστη έξω, θα μου αρέσει η σοκολάτα κάθε μέρα. Τη στιγμή που θα έχει ζέστη έξω, δεν ξέρω αν θα μου αρέσει πια η σοκολάτα. Α, και είναι εγγυημένο ότι τελικά θα έχει ζέστη έξω, ακόμα και αν αυτό είναι μόνο για μία μέρα."
***E**((**EX**.P)**U**(**AG**.Q))
:"Είναι πιθανό ότι: τελικά θα έρθει κάποια στιγμή που θα έχει ζέστη για πάντα (AG.Q) και πριν από αυτή τη στιγμή θα υπάρχει πάντα *κάποιος* τρόπος να μου αρέσει η σοκολάτα την επόμενη ημέρα (EX.P)."

## Σχέση με άλλες λογικές
Η CTL είναι υποσύνολο της CTL*, όπως και του τροπικού μ-λογισμού. Είναι επίσης ενδιαφέρον να επισημανθεί ότι η CTL είναι κομμάτι της Alur, της Χρονικής Λογικής Εναλλασσόμενου Χρόνου (Alternating-time Temporal Logic, ATL) των Henzinger και Kupferman.

Η CTL και η γραμμική χρονική λογική (LTL) είναι υποσύνολα της CTL*. Η CTL και η LTL δεν είναι όμως ισοδύναμες και έχουν κοινό υποσύνολο, το οποίο είναι πραγματικό υποσύνολο κάθε μιας από αυτές.
* Η **FG**.P υπάρχει στην LTL αλλά όχι στη CTL.
* Η **AG**(P\Rightarrow((**EX**.Q)\land(**EX**¬Q))) υπάρχει στη CTL αλλά όχι στην LTL.

## Δείτε επίσης
* Γραμμική χρονική λογική
* CTL*

## Αναφορές
* 
* 
* 
* 

## Εξωτερικοί σύνδεσμοι
* Εκπαιδευτικές διαφάνειες για τη CTL 

Κατηγορία:Λογική για Υπολογιστές
Κατηγορία:Τυπικές μέθοδοι
Κατηγορία:Χρονική λογική