A Note on a Question of Peled and Wilke Regarding Stutter-Invariant LTL
15 November 2000
Peled and Wilke, [PW97], showed that the stutter-invariant languages expressible in linear propositional temporal logic (LTL) are precisely those expressible in LTL without the "next"-time operator. They did so by providing a translation, F, which converts a stutter-invariant LTL formula element to an equivalent formula F(element) not containing the "next" operator. Their F(element) can be exponentially larger than element, with a worst case upper bound of |F(element)|