Λογική υπολογιστικού δένδρου: Διαφορά μεταξύ των αναθεωρήσεων
Περιεχόμενο που διαγράφηκε Περιεχόμενο που προστέθηκε
Γραμμή 41:
Στη [[CTL*]], οι χρονικοί τελεστές μπορούν να αναμιγνύονται ελεύθερα. Στη CTL, ο τελεστής πρέπει πάντα να ομαδοποιείται σε δύο θέσεις: ένας τελεστής μονοπατιού που ακολουθείται από έναν τελεστή κατάστασης. Δείτε τα παραδείγματα παρακάτω. Η [[CTL*]] είναι γνήσια πιο εκφραστική από τη CTL.
=== Ελάχιστο σύνολο από τελεστές ===
Στη CTL υπάρχει ένα ελάχιστο σύνολο από τελεστές. Όλοι οι τύποι της CTL μπορούν να μετασχηματιστούν ώστε να χρησιμοποιούν μόνο αυτούς τους τελεστές, κάτι που είναι χρήσιμο στον [[έλεγχος μοντέλων|έλεγχο μοντέλων]]. Ένα ελάχιστο σύνολο από τελεστές είναι: {false, <math>\or, \neg</math>, '''EG''', '''EU''', '''EX'''}.
Ακολουθούν μερικοί από τους μετασχηματισμούς χρονικών τελεστών:
*'''EF'''<math>\phi</math> == '''E'''[true'''U'''(<math>\phi</math>)] ( επειδή '''F'''<math>\phi</math> == [true'''U'''(<math>\phi</math>)] )
*'''AX'''<math>\phi</math> == <math>\neg</math>'''EX'''(<math>\neg</math><math>\phi</math>)
*'''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>\or</math><math>\psi</math>)] <math>\or</math> '''EG'''(<math>\neg</math><math>\psi</math>) )
== Δείτε επίσης ==
| |||