All the formulas of LTL can be transformed into negation normal form, where
- all negations appear only in front of the atomic propositions,
- only other logical operators true, false, ∧, and ∨ can appear, and
- only the temporal operators X, U, and R can appear.
Using the above equivalences for negation propagation, it is possible to derive the normal form. This normal form allows R, true, false, and ∧ to appear in the formula, which are not fundamental operators of LTL. Note that the transformation to the negation normal form does not blow up the size of the formula. This normal form is useful in translation from LTL to Büchi automaton.
Read more about this topic: Linear Temporal Logic
Famous quotes containing the words negation, normal and/or form:
“Friendship, according to Proust, is the negation of that irremediable solitude to which every human being is condemned.”
—Samuel Beckett (1906–1989)
“The basic thing nobody asks is why do people take drugs of any sort?... Why do we have these accessories to normal living to live? I mean, is there something wrong with society that’s making us so pressurized, that we cannot live without guarding ourselves against it?”
—John Lennon (1940–1980)
““Now what I want is, Facts. Teach these boys and girls nothing but Facts. Facts alone are wanted in life. Plant nothing else, and root out everything else. You can only form the minds of reasoning animals upon Facts: nothing else will ever be of service to them.””
—Charles Dickens (1812–1870)