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:
“We make a mistake forsaking England and moving out into the periphery of life. After all, Taormina, Ceylon, Africa, America—as far as we go, they are only the negation of what we ourselves stand for and are: and we’re rather like Jonahs running away from the place we belong.”
—D.H. (David Herbert)
“What strikes many twin researchers now is not how much identical twins are alike, but rather how different they are, given the same genetic makeup....Multiples don’t walk around in lockstep, talking in unison, thinking identical thoughts. The bond for normal twins, whether they are identical or fraternal, is based on how they, as individuals who are keenly aware of the differences between them, learn to relate to one another.”
—Pamela Patrick Novotny (20th century)
“The man who is admired for the ingenuity of his larceny is almost always rediscovering some earlier form of fraud. The basic forms are all known, have all been practicised. The manners of capitalism improve. The morals may not.”
—John Kenneth Galbraith (b. 1908)