Boolean closure of persistence and fairness property.

Question

It was said in the lecture that, every formula in the boolean closure of safety and liveness (G) and (F) can be brought into the prefix normal forms using cnf and dnf and a constructive proof is given which I understand.

It was also said that every formula in the boolean closure of persistence and fairness conditions can be brought into rabin and street normal form.

Could someone please sketch a constructive proof of that ? I dont see how to get rid of alternations.

Answer 1

The proof works the same way as the one for boolean closure for F and G, i.e., we consider the FG- and GF-formulas as atoms, compute a DNF or CNF and then combine disjunctions or conjunctions of the one or the other kind. This way, we obtain Rabin or Streett formulas.

Comments

How to reduce formulas of the kind FGF and GFG?

---

That is not the question here. Boolean closure of FG and GF does not nest these formulas, we just have a boolean combination of FG and GF formulas.

---

Ah ok, i see my mistake. But what can we do with those formulas? Do we need special acceptance conditions for them ?

---

Or rather special normal forms?

---

No, those formulas do not add anything new since we have (F G F p) <-> (G F p) and (G F G p) <-> (F G p)