Content deleted Content added
→Relations with other logics: Fix CTL/LTL comparison, see LTL page. |
|||
Line 140:
<!-- CTL is complementary to LTL -->
Computation tree logic (CTL) and [[Linear temporal logic]] (LTL) are both a subset of CTL*. CTL and [[Linear temporal logic|LTL]] are not equivalent and they have a common subset, which is a proper subset of both CTL and LTL.
*'''FG'''.P exists in LTL but not in CTL.
*'''AG'''(P<math>\Rightarrow</math>(('''EX'''.Q)<math>\land</math>('''EX'''¬Q))) and '''AG.EF'''.P exist in CTL but not in LTL.
| |||