Modal Mu-Calculus

Abstract

In the previous chapter we saw that modal formulas are not very expressive. They can not capture enduring traits of processes, the properties definable within temporal logic. However, these longer term properties can be viewed as closure conditions on immediate capabilities and necessities that modal logic captures. By permitting recursive modal equations, these temporal properties are expressible as extremal solutions of such equations. The property “whenever a coin is inserted, eventually an item is collected” is expressed using two recursive modal equations with different solutions. In the previous chapter, least and greatest solutions to recursive modal equations were represented using the fixed point quantifiers μZ and υZ. In this chapter we shall explicitly add these connectives to modal logic, thereby providing a very rich temporal logic.