Many optimizations can be done by rewriting the ATL formula. If we can reduce it to simplytrue orfalse then we do not even need to run the certain-zero algorithm. This feature requires an investigation of boolean formula equivalences and an extensible design that can apply rewriting rules repeatedly.

Afew example rewrites:

• A & !A →false
• A | !A →true
• A & (A | B) →A
• A & (!A | B) →A & B
• <<p1>> (true U A) →<<p1>> F A
• <<p1>> F false →false
• ...