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

Η λογική υπολογιστικού δένδρου (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:

EFEGp\Rightarrow AFr

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

EF{\big (}rUq{\big )}

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

Τελεστές

Λογικοί τελεστές

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

Χρονικοί τελεστές

Οι χρονικοί τελεστές είναι οι ακόλουθοι:

Ποσοδείκτες πάνω σε μονοπάτια
- A $\phi$ - Όλα (All): η $\phi$ πρέπει να ισχύει σε όλα τα μονοπάτια που αρχίζουν από την τρέχουσα κατάσταση.
- E $\phi$ - Υπάρχει (Exists): υπάρχει τουλάχιστον ένα μονοπάτι που αρχίζει από την τρέχουσα κατάσταση, στο οποίο να ισχύει η $\phi$ .
Ποσοδείκτες σε συγκεκριμένα μονοπάτια
- X $\phi$ - Επόμενο (Next): η $\phi$ πρέπει να ισχύει στην επόμενη κατάσταση (ο τελεστής αυτός συνήθως συμβολίζεται και σαν N αντί για X).
- G $\phi$ - Καθολικά (Globally): η $\phi$ πρέπει να ισχύει σε όλο το υπόλοιπο μονοπάτι.
- F $\phi$ - Τελικά (Finally): η $\phi$ πρέπει να ισχύει τελικά (κάπου στο υπόλοιπο μονοπάτι).
- $\phi$ U $\psi$ - Μέχρι (Until): η $\phi$ πρέπει να ισχύει τουλάχιστον μέχρι κάποια θέση στην οποία να ισχύει η $\psi$ . Αυτό σημαίνει ότι η $\psi$ θα επαληθευτεί στο μέλλον.
- $\phi$ W $\psi$ - Ασθενές μέχρι (Weak until): η $\phi$ πρέπει να ισχύει μέχρι να ισχύει η $\psi$ . Η διαφορά με τον U είναι ότι δεν εξασφαλίζεται ότι η $\psi$ θα επαληθευτεί ποτέ. Ο τελεστής W κάποιες φορές αποκαλείται και "εκτός αν" ("unless").

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

Ελάχιστο σύνολο τελεστών

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

Ακολουθούν μερικοί από τους μετασχηματισμούς χρονικών τελεστών:

EF $\phi$ == E[trueU( $\phi$ )] ( επειδή F $\phi$ == [trueU( $\phi$ )] )
AX $\phi$ == $\neg$ EX( $\neg$ $\phi$ )
AG $\phi$ == $\neg$ EF( $\neg$ $\phi$ ) == $\neg$ E[trueU( $\neg$ $\phi$ )]
AF $\phi$ == A[trueU $\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<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}$
${\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<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}$

Χαρακτηρισμός της 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 AXAG\phi

EG\phi \equiv \phi \land EXEG\phi

AF\phi \equiv \phi \lor AXAF\phi

EF\phi \equiv \phi \lor EXEF\phi

A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])

E[\phi U\psi ]\equiv \psi \lor (\phi \land EXE[\phi U\psi ])

Παραδείγματα

Έστω ότι "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 $\Rightarrow$ ((EX.Q) $\land$ (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:10.1016/0022-0000(85)90001-7.
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:10.1145/5397.5399. 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 (Αγγλικά)