Λογική υπολογιστικού δένδρου: Διαφορά μεταξύ των αναθεωρήσεων
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
→Ορισμός: fix nonsensical definition copied from english edition |
μ Αντικατάσταση παρωχημένης σύνταξης latex (mw:Extension:Math/Roadmap) |
||
Γραμμή 4:
Η [[κανονική γλώσσα|γλώσσα]] ενός καλώς ορισμένου τύπου σε CTL παράγεται από την ακόλουθη [[γραμματική χωρίς συμφραζόμενα]]:
:<math>\phi::=\bot |\top |p|(\neg\phi)|(\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]</math>
όπου ο <math>p</math> παίρνει τιμές στο σύνολο των ατομικών τύπων (atomic formulas). Δε χρειάζονται όλοι οι σύνδεσμοι - για παράδειγμα οι
<math>\{\neg, \
* <math>A</math> σημαίνει 'σε όλα τα μονοπάτια' ('along All paths') ή ''Αναπόφευκτα'' ''(Inevitably)''
Γραμμή 29:
=== Λογικοί τελεστές ===
Οι λογικοί τελεστές είναι οι συνήθεις: <math>\neg,\
=== Χρονικοί τελεστές ===
Γραμμή 46:
=== Ελάχιστο σύνολο τελεστών ===
Στη CTL υπάρχει ένα ελάχιστο σύνολο από τελεστές. Όλοι οι τύποι της CTL μπορούν να μετασχηματιστούν ώστε να χρησιμοποιούν μόνο αυτούς τους τελεστές, κάτι που είναι χρήσιμο στον [[έλεγχος μοντέλων|έλεγχο μοντέλων]]. Ένα ελάχιστο σύνολο από τελεστές είναι: {false, <math>\
Ακολουθούν μερικοί από τους μετασχηματισμούς χρονικών τελεστών:
Γραμμή 53:
*'''AG'''<math>\phi</math> == <math>\neg</math>'''EF'''(<math>\neg</math><math>\phi</math>) == <math>\neg</math> '''E'''[true'''U'''(<math>\neg</math><math>\phi</math>)]
*'''AF'''<math>\phi</math> == '''A'''[true'''U'''<math>\phi</math>] == <math>\neg</math>'''EG'''(<math>\neg</math><math>\phi</math>)
*'''A'''[<math>\phi</math>'''U'''<math>\psi</math>] == <math>\neg</math>( '''E'''[(<math>\neg</math><math>\psi</math>)'''U'''<math>\neg</math>(<math>\phi</math><math>\
== Σημασιολογία της CTL==
| |||