A syntactical proof of the canonical reactivity form for past linear temporal logic
We present a new proof of the fact that every formula in linear temporal logic with past is equivalent to a formula of the form Graphics where alpha(i) and beta(i) are past formulas, which is known as general canonical reactivity form. The original proof is based on the fact that a finite automaton recognizes an LTL-definable omega-language iff it is counter-free, which was proved in Lenore Zuck's thesis and relies on the theorem of Krohn-Rhodes about cascade decomposition of finite automata. Unlike that, the proof presented in this paper involves only equivalence transformations of LTL formula and makes use of Gabbay's separation theorem, whose proof is based on equivalence transformations too. This makes it possible to obtain the canonical form without resorting to constructions outside LTL with past operators such as automata.
linear temporal logic separation canonical reactivity normal form