Abstract
The propositional µ-calculus is a very expressive language: All languages discussed in this book can be translated to equivalent µ-calculus formulas, but none of them reaches the expressiveness of the µ-calculus. The development of the µ-calculus started in 1975, when Kfoury and Park proved that properties like termination and totality of programs can not be expressed in first order logics [283] (see also Section 6.2.2). For this reason, Park [397], Hitchcock and Park [247], and de Bakker and de Roever [142] introduced a least fixpoint operator to remedy such deficiencies. The resulting formal systems were powerful enough to express important properties like termination, liveness, and deadlocks or starvation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Schneider, K. (2004). Fixpoint Calculi. In: Verification of Reactive Systems. Texts in Theoretical Computer Science. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-10778-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-662-10778-2_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05555-3
Online ISBN: 978-3-662-10778-2
eBook Packages: Springer Book Archive