Continuous Fragment of the mu-Calculus

摘要

In this paper we investigate the Scott continuous fragment of the modal μ-calculus. We discuss its relation with constructivity, where we call a formula constructive if its least fixpoint is always reached in at most ω steps. Our main result is a syntactic characterization of this continuous fragment. We also show that it is decidable whether a formula is continuous.