Mu calculus intuition.

Question

Hi, im missing a bit intuition on forming sentences using the mu calculus. Can someone please make mu calculus formulas and explain their mind process for the states where

1. There exist an infinite path, where the successor state is the negation of the previous state.
2. There exist at least two distinct infinite paths.
3. There exist exactly two distinct infinite paths.
4. States where all path starting from it, must return infinitely often.
5. States that are articulation points. 

I have some ideas about some of them, but I'd rather not confuse people with my thoughts. I feel like it is easier to write these things in CTL* and then translate but i feel that we should not make use of that as mu calculus is more powerful. 

Thanks

Answer 1

Difficult question. I would say that you can follow somehow a recursive programming idea. If you know how to program what you want in a recursive manner using just boolean and modal operators, then you should be able to modify that also to a µ-calculus formula.

The vector µ-calculus, which we did not discuss makes this a bit easier. For example, 1 could be implemented like nu (x,y). (phi & y -> <>(!phi & x)) & (!phi & x ->  <> (phi& y).

I doubt that you can express 2, since you may have a structure with two paths, but these are bisimilar, and therefore satisfy the same µ-calculus formulas. So, I think that formula does not exist. Same with 3.

4 is possible in that you do an intersection of a forward and a backward search, i.e., (mu x. (c | <>x) & (mu y.(c | <:>y)) which gives you all states that are on a cycle where c holds. If c is a particular state, you have what you want.

I am not sure with with articulation points, but you may have a look at https://www.labri.fr/perso/courcell/Book/TheBook.pdf, where monadic second order logic is used to specify graph problems. Since the latter can be translated to µ-calculus, it gives the answers to the graph problems you had in mind.

Comments

Can you give some questions, that we should be able to write in mu calculus?

---

For example, there is a path where at every second/third... point of time p holds? Or there is a path where whenever p holds then also p holds next?

---

Is this correct?
Path which p holds every second point of time:
Let phi_inf= nu x.<>x.

nu x. !p &<><>(x &p & phi_inf) & phi_inf

---

A path where whenever p holds then also p holds next is the persistence property. At some point of time p will hold and then it will always hold after. Or it will never hold so :
(mu y.(nu x. p& <>x) | <>y) | (nu y. y&p -> ! phi_inf)

---

The formula nu x. !p &<><>(x &p & phi_inf) & phi_inf does not make sense: If you forget about phi_inf at first, your formula becomes  nu x. !p & <><>(x&p). I guess you rather mean nu x. p & <><>(x&p); then a fixpoint x must satisfy x = p & <><>(x&p). Thus, x must be a subset of p, but then x&p = x and therefore, you can write nu x. (p & <><>x). That should be the right formula. If you unroll it, you find

    p & <><>(p & <><>(p & <><>x)) = p & <><>p & <><><><>p & <><><><><><>x

A path where whenever p holds, then p also holds next is not just a persistence property, since persistence properties allow a property for a while to do whatever, and then just from a sudden enforce that p must hold forever. Here, we would rather need EG(p->Xp) which is a CTL* formula, but not in CTL. µ-calculus makes a bit effort here, also.