Λογική υπολογιστικού δένδρου: Διαφορά μεταξύ των αναθεωρήσεων
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
Νέα σελίδα: Η '''λογική υπολογιστικού δένδρου''' ('''Computation tree logic''', '''CTL''') είναι μια λογική δ... |
|||
Γραμμή 24:
Το πρόβλημα με αυτόν είναι ότι ο <math>U</math> μπορεί να εμφανίζεται μόνο μαζί με έναν <math>A</math> ή έναν <math>E</math>. Σαν κατασκευαστικά στοιχεία χρησιμοποιεί [[Λογική πρώτου βαθμού|ατομικές προτάσεις]] για να δηλώσει ιδιότητες των καταστάσεων ενός συστήματος. Η CTL στη συνέχεια συνδυάζει αυτές τις προτάσεις σε τύπους χρησιμοποιώντας [[λογικός τελεστής|λογικούς τελεστές]] και [[χρονική λογική|χρονικές λογικές]].
==
=== Λογικοί τελεστές ===
Οι λογικοί τελεστές είναι οι συνήθεις: <math>\neg,\or,\and,\Rightarrow</math> και <math>\Leftrightarrow</math>. Οι τύποι της CTL μπορούν επιπλέον να χρησιμοποιούν με αυτούς τις λογικές σταθερές true (αληθές) και false (ψευδές).
=== Χρονικοί τελεστές ===
Οι χρονικοί τελεστές είναι οι ακόλουθοι:
* Ποσοδείκτες πάνω σε μονοπάτια
** '''A''' <math>\phi</math> - Όλα ('''A'''ll): η <math>\phi</math> πρέπει να ισχύει σε όλα τα μονοπάτια που αρχίζουν από την τρέχουσα κατάσταση.
** '''E''' <math>\phi</math> - Υπάρχει ('''E'''xists): υπάρχει τουλάχιστον ένα μονοπάτι που αρχίζει από την τρέχουσα κατάσταση, στο οποίο να ισχύει η <math>\phi</math>.
* Ποσοδείκτες σε συγκεκριμένα μονοπάτια
** '''X''' <math>\phi</math> - Επόμενο (Ne'''x'''t): η <math>\phi</math> πρέπει να ισχύει στην επόμενη κατάσταση (ο τελεστής αυτός συνήθως συμβολίζεται και σαν '''N''' αντί για '''X''').
** '''G''' <math>\phi</math> - Καθολικά ('''G'''lobally): η <math>\phi</math> πρέπει να ισχύει σε όλο το υπόλοιπο μονοπάτι.
** '''F''' <math>\phi</math> - Τελικά ('''F'''inally): η <math>\phi</math> πρέπει να ισχύει τελικά (κάπου στο υπόλοιπο μονοπάτι).
** <math>\phi</math> '''U''' <math>\psi</math> - Μέχρι ('''U'''ntil): η <math>\phi</math> πρέπει να ισχύει ''τουλάχιστον'' μέχρι κάποια θέση στην οποία να ισχύει η <math>\psi</math>. Αυτό σημαίνει ότι η <math>\psi</math> θα επαληθευτεί στο μέλλον.
** <math>\phi</math> '''W''' <math>\psi</math> - Ασθενές μέχρι ('''W'''eak until): η <math>\phi</math> πρέπει να ισχύει μέχρι να ισχύει η <math>\psi</math>. Η διαφορά με τον '''U''' είναι ότι δεν εξασφαλίζεται ότι η <math>\psi</math> θα επαληθευτεί ποτέ. Ο τελεστής '''W''' κάποιες φορές αποκαλείται και "εκτός αν" ("unless").
Στη [[CTL*]], οι χρονικοί τελεστές μπορούν να αναμιγνύονται ελεύθερα. Στη CTL, ο τελεστής πρέπει πάντα να ομαδοποιείται σε δύο θέσεις: ένας τελεστής μονοπατιού που ακολουθείται από έναν τελεστή κατάστασης. Δείτε τα παραδείγματα παρακάτω. Η [[CTL*]] είναι γνήσια πιο εκφραστική από τη CTL.
== Δείτε επίσης ==
* [[Γραμμική χρονική λογική]]
| |||