μ λογισμός

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση

Ο μ-λογισμόςτροπικός μ λογισμός) είναι μια επέκταση της προτασιακής τροπικής λογικής με έναν τελεστή μ ελάχιστου σταθερού σημείου (fixpoint). Χρησιμοποιείται για να περιγράψει τις ιδιότητες των συστημάτων μεταβάσεων με ετικέτες και να τις επαληθεύσει.

Ο (προτασιακός) μ-λογισμός εφευρέθηκε από τον Ντάνα Σκοτ και τον Τζάκο ντε Μπέκερ[1], και στη συνέχεια αναπτύχθηκε από τον Ντέξτερ Κόζεν για να φτάσει στην έκδοση που χρησιμοποιείται σήμερα.

Πολλές χρονικές λογικές μπορούν να κωδικοποιηθούν στο μ-λογισμό, όπως η LTL, η CTL και η CTL*.[2]

Παραπομπές[Επεξεργασία | επεξεργασία κώδικα]

  1. Kozen σελ.333
  2. Clarke σελ.108, Theorem 6; Emerson σελ.196

Αναφορές[Επεξεργασία | επεξεργασία κώδικα]

Στο λήμμα αυτό έχει ενσωματωθεί κείμενο από το λήμμα Mu calculus της Αγγλόγλωσσης Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).