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 ∧_i◇□α_i → ◇□β_i, where α_i and β_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 co-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.