Λογική υπολογιστικού δένδρου: Διαφορά μεταξύ των αναθεωρήσεων
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
Γραμμή 75:
# <math>\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)</math>
# <math>\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)</math>
=== Χαρακτηρισμός της CTL===
Οι κανόνες 10-15 παραπάνω αναφέρονται σε υπολογιστικά μονοπάτια σε μοντέλα και είναι αυτοί που τελικά χαρακτηρίζουν το "Υπολογιστικό Δένδρο", είναι βεβαιώσεις σχετικά με τη φύση του υπολογιστικού δένδρου με άπειρο βάθος και ρίζα τη δεδομένη κατάσταση <math>s</math>.
=== Σημασιολογική ισοδυναμία ===
Οι τύποι της CTL <math>\phi</math> και <math>\psi</math> λέγονται σημασιολογικά ισοδύναμοι αν κάθε κατάσταση σε κάθε μοντέλο που ικανοποιεί τον ένα, ικανοποιεί και τον άλλο.
:Αυτό δηλώνεται <math>\phi \equiv \psi</math>
Φαίνεται ότι οι A και E είναι δυικοί (δηλαδή ο ένας μπορεί να οριστεί με βάση τον άλλο), όπως και οι G και F, εφόσον είναι ο καθολικός και ο υπαρξιακός ποσοδείκτης αντίστοιχα στα υπολογιστικά δένδρα.
Οι νόμοι του Ντε Μόργκαν μπορούν να τυποποιηθούν στη CTL όπως στο παρακάτω παράδειγμα:
:<math>\neg AF\phi \equiv EG\neg\phi</math>
:<math>\neg EF\phi \equiv AG\neg\phi</math>
:<math>\neg AX\phi \equiv EX\neg\phi</math>
Από αυτά τα δεδομένα προκύπτει ότι:
:<math>AF\phi \equiv A[\top U \phi]</math>
:<math>EF\phi \equiv E[\top U \phi]</math>
Στην πραγματικότητα, μπορεί να δειχθεί, με τη χρήση αυτών των ταυτοτήτων, ότι ένα υποσύνολο των χρονικών συνδέσμων της CTL αρκεί αν περιέχει τον <math>EU</math>, τουλάχιστον έναν από τους <math>\{AX,EX\}</math> και τουλάχιστον έναν από τους <math>\{EG,AF,AU\}</math>.
Κάποιες επιπλέον σημαντικές ταυτότητες:
:<math>AG\phi \equiv \phi \land AX AG \phi</math>
:<math>EG\phi \equiv \phi \land EX EG \phi</math>
:<math>AF\phi \equiv \phi \lor AX AF \phi</math>
:<math>EF\phi \equiv \phi \lor EX EF \phi</math>
:<math>A[\phi U \psi] \equiv \psi \lor (\phi \land AX A [\phi U \psi])</math>
:<math>E[\phi U \psi] \equiv \psi \lor (\phi \land EX E [\phi U \psi])</math>
== Δείτε επίσης ==
| |||