# 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?

-
For C: it lies in the alternation-free fragment, which has linear time model-checking complexity in the product of sizes $O(|\mathfrak{M}|\cdot|F|)$ where $\mathfrak{M}$ is the model and $F$ the formula. –  Sylvain Dec 6 '12 at 23:06

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.

-
Just pointing out: The conjunctive nu-calculus has an operator $\not\to^a$ which states that there is no $a$ transition, but this is not expressible in the OP's logic. –  Dave Clarke Dec 6 '12 at 8:43
Thank you for this relevant reference! I'll read it carefully –  Mn10 Dec 6 '12 at 14:11

I don't have any proofs, but I suspect the following.

1. The satisfiability problem is trivial: all closed formula are satisfiable. This can be demonstrated by constructing a model in the following way based on the structure of the formula. Assume that $s$ is the state which is the current focus of the algorithm. Start from a model with a single state and no transitions. In state $s$:

• For $p$, set $p$ in the current state. In fact, I can set all $p$ to be true in all states, as I can never ask whether $\lnot p$ holds.
• For $F\land G$, process $F$ starting from state $s$, then again from state $s$, process $G$.
• For $[a]F$ if there is an $a$ transition, follow it and ensure that $F$ holds in the resulting state. Otherwise, add a new state $t$ and an $a$ transition to it from state $s$, and ensure that $F$ is satisfied in $s$.
• For $\nu X.F$, remember that $X$ corresponds state $s$. Perform the construction to satisfy $F$, and whenever $X$ is seen in $F$ make the state the same as the one corresponding to $X$.
2. A) is true. The above construction can be modified to ensure that if an $a$ edge exists already from a given state.

3. B) is constant time, as all (closed) formula are satisfiable. (Or time proportional to the size of the formula if you need to check that it is well-formed.)

Not sure about C). Probably not very complex.

-
I don't see why all formulae in the calculus are closed. –  Vijay D Dec 6 '12 at 8:19
@VijayD: I didn't say that all formula are closed. I said that all close formula are satisfiable. –  Dave Clarke Dec 6 '12 at 8:21
Thank you Dave for this insightful comment. I kind of agree with your suggestion. However I had in mind, using propositional letters p, to have litterals, i.e., p and \neg p for all propositions symbols. Of course there are now UNSAT formulas, but still your construction seems useful. –  Mn10 Dec 6 '12 at 14:13
I would just modify the syntax to have $p$ and $\neg p$. This is a common thing to do. –  Dave Clarke Dec 6 '12 at 14:30