P. Cousot, Methods and Logics for Proving Programs

Comparison of LTL and CTL.

Abstract: Temporal logic is one type of modal logic for reasoning about temporal properties. In the last twenty years, it became a widely used tool in specifying and verifying properties of concurrent systems. Among many variants of temporal logics proposed so far, the most popular two are linear time temporal logic (LTL) and branching time temporal logic (BTL). In the following survey, we present a comparison of the two logics from several viewpoints.