Modal Mu-Calculus

  • Colin Stirling
Part of the Texts in Computer Science book series (TCS)

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.

Keywords

Modal Logic Free Variable Safety Property Liveness Property Modal Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 2001

Authors and Affiliations

  • Colin Stirling
    • 1
  1. 1.Division of InformaticsUniversity of EdinburghEdinburghUK

Personalised recommendations