Λογική υπολογιστικού δένδρου
Το λήμμα παραθέτει τις πηγές του αόριστα, χωρίς παραπομπές. |
Η λογική υπολογιστικού δένδρου (Computation tree logic, CTL) είναι μια λογική διακλαδιζόμενου χρόνου (branching-time), το οποίο σημαίνει ότι το μοντέλο της για το χρόνο είναι μια δενδρική δομή, στην οποία το μέλλον δεν έχει οριστεί αλλά υπάρχουν διαφορετικά μονοπάτια σε αυτό και κάθε ένα από αυτά τα μονοπάτια μπορεί να είναι ένα μονοπάτι που θα πραγματοποιηθεί. Χρησιμοποιείται στην τυπική επαλήθευση λογισμικού ή υλικού, συνήθως από λογισμικό που ονομάζεται ελεγκτής μοντέλων. Το λογισμικό αυτό προσδιορίζει αν το λογισμικό ή το υλικό που ελέγχεται έχει κάποιες συγκεκριμένες ιδιότητες ασφάλειας (safety) ή ζωτικότητας (liveness). Ανήκει στην κατηγορία των χρονικών λογικών, όπως και η γραμμική χρονική λογική.
Σύνταξη της CTL
ΕπεξεργασίαΗ γλώσσα ενός καλώς ορισμένου τύπου σε CTL παράγεται από την ακόλουθη γραμματική χωρίς συμφραζόμενα:
όπου ο παίρνει τιμές στο σύνολο των ατομικών τύπων (atomic formulas). Δε χρειάζονται όλοι οι σύνδεσμοι - για παράδειγμα οι αποτελούν πλήρες σύνολο συνδέσμων, με τους υπόλοιπους να μπορούν να οριστούν με βάση αυτούς.
- σημαίνει 'σε όλα τα μονοπάτια' ('along All paths') ή Αναπόφευκτα (Inevitably)
- σημαίνει 'σε ένα τουλάχιστον μονοπάτι' ('along at least - there Exists - one path') ή Πιθανόν (possibly)
Για παράδειγμα, ο εξής τύπος είναι ένας καλώς ορισμένος τύπος της CTL:
Ο παρακάτω δεν είναι καλώς ορισμένος τύπος της CTL:
Το πρόβλημα με αυτόν είναι ότι ο μπορεί να εμφανίζεται μόνο μαζί με έναν ή έναν . Σαν κατασκευαστικά στοιχεία χρησιμοποιεί ατομικές προτάσεις για να δηλώσει ιδιότητες των καταστάσεων ενός συστήματος. Η CTL στη συνέχεια συνδυάζει αυτές τις προτάσεις σε τύπους χρησιμοποιώντας λογικούς τελεστές και χρονικές λογικές.
Τελεστές
ΕπεξεργασίαΛογικοί τελεστές
ΕπεξεργασίαΟι λογικοί τελεστές είναι οι συνήθεις: και . Οι τύποι της CTL μπορούν επιπλέον να χρησιμοποιούν με αυτούς τις λογικές σταθερές true (αληθές) και false (ψευδές).
Χρονικοί τελεστές
ΕπεξεργασίαΟι χρονικοί τελεστές είναι οι ακόλουθοι:
- Ποσοδείκτες πάνω σε μονοπάτια
- A - Όλα (All): η πρέπει να ισχύει σε όλα τα μονοπάτια που αρχίζουν από την τρέχουσα κατάσταση.
- E - Υπάρχει (Exists): υπάρχει τουλάχιστον ένα μονοπάτι που αρχίζει από την τρέχουσα κατάσταση, στο οποίο να ισχύει η .
- Ποσοδείκτες σε συγκεκριμένα μονοπάτια
- X - Επόμενο (Next): η πρέπει να ισχύει στην επόμενη κατάσταση (ο τελεστής αυτός συνήθως συμβολίζεται και σαν N αντί για X).
- G - Καθολικά (Globally): η πρέπει να ισχύει σε όλο το υπόλοιπο μονοπάτι.
- F - Τελικά (Finally): η πρέπει να ισχύει τελικά (κάπου στο υπόλοιπο μονοπάτι).
- U - Μέχρι (Until): η πρέπει να ισχύει τουλάχιστον μέχρι κάποια θέση στην οποία να ισχύει η . Αυτό σημαίνει ότι η θα επαληθευτεί στο μέλλον.
- W - Ασθενές μέχρι (Weak until): η πρέπει να ισχύει μέχρι να ισχύει η . Η διαφορά με τον U είναι ότι δεν εξασφαλίζεται ότι η θα επαληθευτεί ποτέ. Ο τελεστής W κάποιες φορές αποκαλείται και "εκτός αν" ("unless").
Στη CTL*, οι χρονικοί τελεστές μπορούν να αναμιγνύονται ελεύθερα. Στη CTL, ο τελεστής πρέπει πάντα να ομαδοποιείται σε δύο θέσεις: ένας τελεστής μονοπατιού που ακολουθείται από έναν τελεστή κατάστασης. Δείτε τα παραδείγματα παρακάτω. Η CTL* είναι γνήσια πιο εκφραστική από τη CTL.
Ελάχιστο σύνολο τελεστών
ΕπεξεργασίαΣτη CTL υπάρχει ένα ελάχιστο σύνολο από τελεστές. Όλοι οι τύποι της CTL μπορούν να μετασχηματιστούν ώστε να χρησιμοποιούν μόνο αυτούς τους τελεστές, κάτι που είναι χρήσιμο στον έλεγχο μοντέλων. Ένα ελάχιστο σύνολο από τελεστές είναι: {false, , EG, EU, EX}.
Ακολουθούν μερικοί από τους μετασχηματισμούς χρονικών τελεστών:
- EF == E[trueU( )] ( επειδή F == [trueU( )] )
- AX == EX( )
- AG == EF( ) == E[trueU( )]
- AF == A[trueU ] == EG( )
- A[ U ] == ( E[( )U ( )] EG( ) )
Σημασιολογία της CTL
ΕπεξεργασίαΟρισμός
ΕπεξεργασίαΟι τύποι της CTL ερμηνεύονται με συστήματα μεταβάσεων (Transition Systems), όπως περιγράφεται τυπικά παρακάτω.
Έστω ότι είναι ένα μοντέλο για τη CTL
- with όπου F είναι το σύνολο των καλώς ορισμένων τύπων στην κανονική γλώσσα .
Τότε η σημασιολογική σχέση ορίζεται από δομική επαγωγή (Structural Induction) στην :
Χαρακτηρισμός της CTL
ΕπεξεργασίαΟι κανόνες 10-15 παραπάνω αναφέρονται σε υπολογιστικά μονοπάτια σε μοντέλα και είναι αυτοί που τελικά χαρακτηρίζουν το "Υπολογιστικό Δένδρο", είναι βεβαιώσεις σχετικά με τη φύση του υπολογιστικού δένδρου με άπειρο βάθος και ρίζα τη δεδομένη κατάσταση .
Σημασιολογική ισοδυναμία
ΕπεξεργασίαΟι τύποι της CTL και λέγονται σημασιολογικά ισοδύναμοι αν κάθε κατάσταση σε κάθε μοντέλο που ικανοποιεί τον ένα, ικανοποιεί και τον άλλο.
- Αυτό δηλώνεται
Φαίνεται ότι οι A και E είναι δυικοί (δηλαδή ο ένας μπορεί να οριστεί με βάση τον άλλο), όπως και οι G και F, εφόσον είναι ο καθολικός και ο υπαρξιακός ποσοδείκτης αντίστοιχα στα υπολογιστικά δένδρα.
Οι νόμοι του Ντε Μόργκαν μπορούν να τυποποιηθούν στη CTL όπως στο παρακάτω παράδειγμα:
Από αυτά τα δεδομένα προκύπτει ότι:
Στην πραγματικότητα, μπορεί να δειχθεί, με τη χρήση αυτών των ταυτοτήτων, ότι ένα υποσύνολο των χρονικών συνδέσμων της CTL αρκεί αν περιέχει τον , τουλάχιστον έναν από τους και τουλάχιστον έναν από τους .
Κάποιες επιπλέον σημαντικές ταυτότητες:
Παραδείγματα
ΕπεξεργασίαΈστω ότι "P" σημαίνει "μου αρέσει η σοκολάτα" και Q σημαίνει "έχει ζέστη έξω."
- AG.P
- "Θα μου αρέσει η σοκολάτα από τώρα, ό,τι και να γίνει."
- EF.P
- "Μπορεί να μου αρέσει η σοκολάτα κάποια μέρα, τουλάχιστον για μία μέρα."
- AF.EG.P
- "Είναι πάντα πιθανό (AF) ότι ξαφνικά θα αρχίσει να μου αρέσει η σοκολάτα για όλον τον υπόλοιπο χρόνο." (Σημείωση: όχι μόνο για την υπόλοιπη ζωή μου, επειδή αυτή είναι πεπερασμένη, ενώ ο G είναι άπειρος).
- EG.AF.P
- "Αυτή είναι μια σημαντική στιγμή στη ζωή μου. Ανάλογα με το τι θα συμβεί στη συνέχεια (E), είναι πιθανό ότι για όλον τον υπόλοιπο χρόνο (G), θα υπάρχει πάντα κάποια στιγμή στο μέλλον (AF) που θα μου αρέσει η σοκολάτα. Όμως, αν συμβεί κάτι λάθος την επόμενη στιγμή, δεν γνωρίζω αν θα μου αρέσει ποτέ η σοκολάτα."
- A(PUQ)
- "Από τώρα και μέχρι να έχει ζέστη έξω, θα μου αρέσει η σοκολάτα κάθε μέρα. Τη στιγμή που θα έχει ζέστη έξω, δεν ξέρω αν θα μου αρέσει πια η σοκολάτα. Α, και είναι εγγυημένο ότι τελικά θα έχει ζέστη έξω, ακόμα και αν αυτό είναι μόνο για μία μέρα."
- 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 ((EX.Q) (EX¬Q))) υπάρχει στη CTL αλλά όχι στην LTL.
Δείτε επίσης
ΕπεξεργασίαΑναφορές
Επεξεργασία- Michael Huth and Mark Ryan (2004). Logic in Computer Science (Second Edition). Cambridge University Press, σελ. 207. ISBN 0-521-54310-X. https://archive.org/details/logiccomputersci00huth_960.
- Emerson, E. A.; Halpern, J. Y. (1985). «Decision procedures and expressiveness in the temporal logic of branching time». Journal of Computer and System Sciences 30 (1): 1–24. doi: .
- Clarke, E. M.; Emerson, E. A.; Sistla, A. P. (1986). «Automatic verification of finite-state concurrent systems using temporal logic specifications». ACM Transactions on Programming Languages and Systems 8 (2): 244–263. doi:. https://archive.org/details/sim_acm-transactions-on-programming-languages-and-systems_1986-04_8_2/page/244.
- Emerson, E. A. (1990). «Temporal and modal logic». Στο: J. van Leeuwen. Handbook of Theoretical Computer Science, vol. B. MIT Press. σελίδες 955–1072. ISBN 0-262-22039-3.
Εξωτερικοί σύνδεσμοι
Επεξεργασία- Εκπαιδευτικές διαφάνειες για τη CTL (Αγγλικά)