μ λογισμός

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

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

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

Αναφορές

• Clarke, Jr., Edmund M.; Orna Grumberg, Doron A. Peled (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:10.1016/0304-3975(82)90125-6. 
• Bradfield, Julian and 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