Fragments of the mu calculus I would like to know if somebody has studied the following very simple fragment of the modal mu-calculus:

$$F::= X \;| \; p \; | \; F \wedge G \; | \; [a]F \; | \; \nu X.F$$

where p ranges over propositional letters. In other words this is the mu-calculus where no disjunction, diamond or least fixed point operators are ever used.

This is a almost trivial fragment, of course. But i'm interested in the following two questions:

A) Is it true that if F is satisfiable, then it is satifiable in a finite model such that every vertex $X$ in the labeled Kripke structure has at most one $a$-labeled children?
i.e., such that $X\xrightarrow{a}Y$ and $X\xrightarrow{a}Z$ then $Y=Z$?

B) What is the complexity of the satisfiablity problem for this logic?

C) What is the complexity of model checking?
To answer the first part of your question 


  Modal specifications are a syntactic fragment of the Mu-calculus, Guillaume Feuillade, 2005.


From the introductory paragraph


  As a consequence, we define a syntactic fragment of the Mu-calculus, called the conjunctive modal Nu calculus, ...In this report, we prove that the conjunctive modal Nu-calculus and modal specifications have the same expressive power and that we can switch between both without loss of generality. We also prove that the set of models of a modal specification is a lattice with finite models as extrema. 


You should examine the details, particularly because the notion of a modal specification is not standard, and is defined in the article.