μ λογισμός
Ο μ-λογισμός (ή τροπικός μ λογισμός) είναι μια επέκταση της προτασιακής τροπικής λογικής με έναν τελεστή μ ελάχιστου σταθερού σημείου (fixpoint). Χρησιμοποιείται για να περιγράψει τις ιδιότητες των συστημάτων μεταβάσεων με ετικέτες και να τις επαληθεύσει.
Ο (προτασιακός) μ-λογισμός εφευρέθηκε από τον Ντέινα Σκοτ και τον Τζάκο ντε Μπέκερ[1], και στη συνέχεια αναπτύχθηκε από τον Ντέξτερ Κόζεν για να φτάσει στην έκδοση που χρησιμοποιείται σήμερα.
Πολλές χρονικές λογικές μπορούν να κωδικοποιηθούν στο μ-λογισμό, όπως η LTL, η CTL και η CTL*.[2][3]
Παραπομπές Επεξεργασία
- ↑ Kozen 1983, σελ. 333.
- ↑ Clarke, Jr., Grumberg & Peled 1999, σελ. 108.
- ↑ Emerson 1996, σελ. 196.
Αναφορές Επεξεργασία
- Clarke, Jr., Edmund M.· Grumberg, Orna· Peled, Doron A. (1999). Model Checking. Cambridge, Massachusetts, USA: MIT press. ISBN 0-262-03270-8.
- Stirling, Colin. (2001). Modal and Temporal Properties of Processes. New York, Berlin, Heidelberg: Springer Verlag. ISBN 0-387-98717-7.
- Emerson, E. Allen (1996). «Model Checking and the Mu-calculus». Descriptive Complexity and Finite Models. American Mathematical Society, pp. 185–214. ISBN 0-8218-0517-7.
- Kozen, Dexter (1983). «Results on the Propositional μ-Calculus». Theoretical Computer Science 27 (3): 333–354. doi:.
- Bradfield, Julian; Stirling, Colin (2006). Modal mu-calculi. Elsevier, σελ. 721–756. http://homepages.inf.ed.ac.uk/jcb/Research/pubs.html#mlh-chapter.
- Videolectures.net - ANU Logic Summer School '09