Acceptance condition in LTL to Mu-automaton

Question

Hello,

In exam solution 2019.02.13, question 7.a, while translating LTL formula to mu-automaton, we get multiple acceptance conditions in the process i.e. GF(q0->b), GF(q0->q1), GF[q2 -> c] and GF[q3 | a]. But in the solution, we choose only GF(q2->c) and GF[q0->b] while the rest are ignored. Is there any reason why we choose only two of them?

Thank You. Regards

Answer 1

The formula considered in that exam problem was G[a SU b] | [F c WB a], so that we abbreviate

 q0 = [a SU b]   / trans: q0<-> b | a & Xq0       / constraint: GF[q0→b]
 q1 = G q0       / trans: q1 <-> q0 & Xq1         / constraint: GF[q0→q1]
 q2 = F c        / trans: q2 <-> c | Xq2          / constraint: GF[q2→c]
 q3 = [q2 WB a]  / trans: q3 <-> !a & (q2 | Xq3)  / constraint: GF[q3∨a]  

You may add all four constraints, but as explained on slides 81-83, it is sufficient to list the constraints only for negative occurrences of weak and positive occurrences of strong operators. Hence, we only need the constraints for q0 and q2. It is also correct to add both constrains for q1 and q3 or one of them. See also the examples after slide 83.

Comments

Okay so we can get rid of constraints for positive occurrence of weak operator and negative occurrence of strong operator?

---

right, these are redundant (hence, harmless to add, but of no use)

---

thanks appreciate it