Questions: Temporal Logic

Question 1

The LTL formula GF p means 'p holds infinitely often on every execution trace.' Which statement about this property is correct?

• A. It is expressible in CTL as AGF p, making LTL and CTL equivalent for this property
• B. It is expressible in CTL as AGAF p, which is distinct from the LTL formula
• C. It cannot be expressed in CTL because CTL cannot quantify over all positions on a single infinite trace
• D. It is equivalent to AF p in CTL since CTL handles fairness natively

Answer: (C)

GF p (p holds infinitely often) is a canonical LTL property that has no direct CTL equivalent. CTL path quantifiers (A, E) must immediately precede temporal operators (G, F, X, U) — you cannot nest them freely. The CTL formula AGAF p means 'from every reachable state, on all paths from there, p eventually holds,' which is a stronger property than 'p holds infinitely often on traces.' This incomparability — where LTL can express trace-level properties that CTL cannot — is why neither logic subsumes the other.

Question 2

In CTL, what is the difference between AG φ and EG φ at a given state s?

• A. No difference — both say φ holds at every future state reachable from s
• B. AG φ means φ holds on all paths from s; EG φ means φ holds on some path from s; they can have different truth values at s
• C. AG φ is the LTL interpretation and EG φ is the CTL interpretation of the same property
• D. AG φ means φ holds at all states globally in the model; EG φ is restricted to successors of s

Answer: (B)

CTL path quantifiers (A = 'on all paths', E = 'on some path') fundamentally change meaning. AG φ is true at s if φ holds at every state on every computation path from s — a universal claim. EG φ is true at s if there exists at least one computation path from s where φ holds at every state. A branching system can have states where one path maintains φ indefinitely (making EG φ true) while another path eventually violates φ (making AG φ false). This distinction only makes sense in CTL's branching-time view of computation.

Question 3

CTL is strictly more expressive than LTL because CTL adds path quantifiers A and E that LTL lacks.

• T. True
• F. False

Answer: False

LTL and CTL are *incomparable* in expressiveness — neither is a subset of the other. Some properties are expressible in LTL but not CTL (e.g., GF p, 'p holds infinitely often'), and some are expressible in CTL but not LTL (e.g., EF safe, 'there exists a path where safe is eventually reached' — a branching reachability property that quantifies over the tree structure). The key insight is that LTL reasons about individual traces while CTL reasons about the branching structure of all possible executions; these are fundamentally different perspectives, not one extending the other.

Question 4

Temporal logic model checking for finite-state systems is decidable, meaning there is an algorithm that always terminates with a correct yes/no answer.

• T. True
• F. False

Answer: True

For finite-state systems (Kripke structures with finitely many states), both LTL and CTL model checking are decidable and run in polynomial time in the size of the model. The main practical challenge is state space explosion — the model size grows exponentially in the number of system variables — but this is an engineering challenge, not a decidability barrier. Model checking becomes undecidable for infinite-state systems in general, but the finite-state case, which covers most hardware and many software verification problems, is algorithmically tractable.

Question 5

Explain in your own words why LTL and CTL are incomparable in expressiveness, rather than one being a subset of the other.

Model answer: LTL treats time as a single infinite sequence (a trace) and cannot distinguish between 'all paths' and 'some path.' CTL treats time as a branching tree and requires path quantifiers before every temporal operator, which prevents it from making statements about a single infinite trace. LTL can say 'p holds infinitely often on this trace' (GF p) — a property about the long-run behavior of one path — while CTL cannot express this directly. Conversely, CTL can say 'there exists some path where q is eventually reached' (EF q) — a branching reachability property — while LTL cannot, because LTL quantifies implicitly over all traces. Each logic captures something the other misses.

The incomparability reflects the fundamental design difference: LTL's linear-time view is better at trace-level properties like fairness and liveness along a single execution, while CTL's branching-time view is better at reachability and safety properties over the full state space. Neither view strictly dominates. CTL* was developed as a unifying logic that subsumes both, but at a computational cost.