6 - HML with recursion

Summary

Introduction

An HML formula can only describe a finite part of the overall behaviour of a process. In fact, as each modal operator allows us to explore the effect of taking one step in the behaviour of a process, using a single HML formula we can only describe properties of a fixed small part of the computations of a process. As those who solved Exercise 5.13 have already discovered, how much of the behaviour of a process we can explore using a single formula is entirely determined by its so-called modal depth, i.e. by the maximum nesting of modal operators in it. For example, the formula ([a]〈a〉ff) ∨ 〈b〉tt has modal depth 2, and checking whether a process satisfies it involves only an analysis of its sequences of transitions whose length is at most 2. (We will return to this issue in Section 6.6, where a formal definition of the modal depth of a formula will be given.)

However, we often wish to describe properties that describe a state of affairs that may or must occur in arbitrarily long computations of a process. If we want to express properties such as, for example, that a process is always able to perform a given action, we have to extend the logic. As the following example indicates, one way of doing so is to allow for infinite conjunctions and disjunctions in our property language.