<p>To answer the first part of your question </p>

<blockquote>
  <p><a href="http://hal.inria.fr/inria-00070396/PDF/RR-5612.pdf" rel="nofollow">Modal specifications are a syntactic fragment of the Mu-calculus</a>, Guillaume Feuillade, 2005.</p>
</blockquote>

<p>From the introductory paragraph</p>

<blockquote>
  <p>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. </p>
</blockquote>

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

CC BY-SA 3.0
2012-12-06T08:43:15.607Z
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
CC BY-SA 3.0
2012-12-06T14:11:11.843Z
Thank you for this relevant reference! I'll read it carefully
Mn10
CC BY-SA 3.0
2012-12-06T08:32:52.527Z
2012-12-06T08:32:52.527Z
Vijay D
<p>I don't have any proofs, but I suspect the following. </p>

<ol>
<li><p>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$:</p>

<ul>
<li>For $p$, set $p$ in the current state. <em>In fact, I can set all $p$ to be true in all states, as I can never ask whether $\lnot p$ holds.</em></li>
<li>For $F\land G$, process $F$ starting from  state $s$, then again from state $s$, process $G$.</li>
<li>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$. </li>
<li>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$.</li>
</ul></li>
<li><p>A) is true. The above construction can be modified to ensure that if an $a$ edge exists already from a given state.</p></li>
<li><p>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.)</p></li>
</ol>

<p>Not sure about C). Probably not very complex.</p>

CC BY-SA 3.0
2012-12-06T08:19:34.327Z
I don't see why all formulae in the calculus are closed.
Vijay D
CC BY-SA 3.0
2012-12-06T08:21:46.027Z
@VijayD: I didn't say that all formula are closed. I said that all close formula are satisfiable.
Dave Clarke
CC BY-SA 3.0
2012-12-06T14:13:15.467Z
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
CC BY-SA 3.0
2012-12-06T14:30:57.183Z
I would just modify the syntax to have $p$ and $\neg p$. This is a common thing to do.
Dave Clarke
CC BY-SA 3.0
2012-12-05T18:49:07.623Z
2012-12-06T12:52:04.443Z
2012-12-06T12:52:04.443Z
Dave Clarke
<p>I would like to know if somebody has studied the following very simple fragment of the modal mu-calculus:</p>

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

<p>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.</p>

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

<p>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$?</p>

<p>B) What is the complexity of the satisfiablity problem for this logic?</p>

<p>C) What is the complexity of model checking?</p>

CC BY-SA 3.0
2012-12-06T23:06:27.567Z
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
<lo.logic><mu-calculus>
Fragments of the mu calculus
Mn10
# Fragments of the mu calculus

(Asked by: username_0 on 2012-12-05)

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?

**Tags:** lo.logic, mu-calculus
> **Comments:**
> **username_1**: 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.  

---

## 2 answers

### Answer by username_2 on 2012-12-06. Score: 2

To answer the first part of your question

> [Modal specifications are a syntactic fragment of the Mu-calculus](http://hal.inria.fr/inria-00070396/PDF/RR-5612.pdf), 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.

> **Comments:**
> **username_3**: 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.  
> **username_0**: Thank you for this relevant reference! I'll read it carefully  

---

### Answer by username_3 on 2012-12-05. Score: 0

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.

> **Comments:**
> **username_2**: I don't see why all formulae in the calculus are closed.  
> **username_3**: @VijayD: I didn't say that all formula are closed. I said that all close formula are satisfiable.  
> **username_0**: 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.  
> **username_3**: I would just modify the syntax to have $p$ and $\neg p$. This is a common thing to do.  

---

