View Related Documents

Abstract

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.

Keywords  mu-calculus - automata - Scott continuity - constructive fixpoints - preservation results

Fulltext Preview

Image of the first page of the fulltext document