Observational Mu-Calculus

ful framework is full second-order logic; however, this is intractable, in many ways. Monadic second-order logic is a restriction which has a much more amenable theory; it is also used in at least one serious verification environment[3]. It can be argued that second-order quantification is too hard to understand, even for an assembly-language logic. It is also arguable that since the popular temporal logics are all expressible in terms of fixpoints, it is unnecessary to go beyond fixpoints to second order, even monadic. This would suggest the use of first-order logic with fixpoints, a logic much studied in finite model theory, though less so in the mainstream verification community. However, we maintain that all these logics have one feature, which is not shared by traditional temporal logics, and which we consider undesirable: they all have variables ranging over `states', so that a formula can capture states and keep them for later inspection. Temporal logics, including the modal mu