Multi-valued Fixpoint Logic

We investigate multi-valued fixpoint logic, an extension of the classical mu-calculus where logical values range over a fixed complete lattice A equipped with monotone operations as connectives. We present equivalent game semantics for the logic and use it to investigate the case when A is the unit interval [0,1] with connectives ½ and floor(_). It turns out that the resulting logic is equivalent to the fragment of the recently introduced countdown mu-calculus in which countdown operators are not nested. If time permits, we will discuss how the choice of the both lattice and connectives may affect expressivity and (un)decidability of satisfiability and model-checking.