Relations With Other Logics
LTL can be shown to be equivalent to the monadic first-order logic of order, FO—a result known as Kamp's theorem— or equivalently star-free languages.
Computation tree logic (CTL) and Linear temporal logic (LTL) are both a subset of CTL*. CTL and LTL are not equivalent and they have a common subset, which is a proper subset of both CTL and LTL. For example,
- No formula in CTL can define the language that is defined by the LTL formula F(G p).
- No formula in LTL can define the language that is defined by the CTL formula AG( p → (EXq ∧ EX¬q) ).
Read more about this topic: Linear Temporal Logic
Famous quotes containing the words relations and/or logics:
“So soon did we, wayfarers, begin to learn that man’s life is rounded with the same few facts, the same simple relations everywhere, and it is vain to travel to find it new.”
—Henry David Thoreau (1817–1862)
“When logics die,
The secret of the soil grows through the eye,
And blood jumps in the sun;
Above the waste allotments the dawn halts.”
—Dylan Thomas (1914–1953)