A note on stutter-invariant PLTL

Peled and Wilke proved that every stutter-invariant propositional linear temporal property is expressible in Propositional Linear Temporal Logic (PLTL) without ◯ (next) operators. To eliminate next operators, a translation τ which converts a stutter-invariant PLTL formula ϕ to an equivalent formula τ(ϕ) not containing ◯ operators has been given. By τ, for any formula , where φ contains no ◯ operators, a formula with the length of O(n4|φ|) is always produced, where n is the number of distinct propositions in ϕ, and |φ| is the number of symbols appearing in φ. Etessami presented an improved translation τ′. By τ′, for , a formula with the length of O(n×n2|φ|) is always produced. We further improve Etessami's result in the worst case to O(n×n2|φ|) by providing a new translation τ″, and we show that the worst case will never occur.