Questions: Temporal Logic: LTL and CTL

Question 1

The LTL formula G(request -> F grant) expresses which property?

• A. If a request occurs, a grant must occur in the very next state
• B. On every execution path, whenever a request occurs, a grant eventually follows at some future point
• C. There exists some path where every request is followed by a grant
• D. Grants always precede requests

Answer: (B)

G means 'globally' (at every point in time) and F means 'finally' (at some future point). So G(request -> F grant) says: at every moment, if request holds, then there exists some future moment where grant holds. LTL formulas are implicitly universally quantified over all paths, so this must hold on every possible execution. This is a classic liveness property — something good eventually happens.

Question 2

LTL and CTL have the same expressive power — any property expressible in one can be expressed in the other.

• T. True
• F. False

Answer: False

LTL and CTL are incomparable in expressiveness. The CTL formula AG(EF restart) ('from every reachable state, there exists a path to restart') cannot be expressed in LTL because LTL cannot mix path quantifiers with temporal operators at arbitrary nesting depths. Conversely, the LTL formula F(G p) ('eventually p holds forever') cannot be expressed in CTL. The logic CTL* subsumes both, combining branching-time quantifiers with arbitrary linear-time operators.

Question 3

Explain the difference between the safety property G(not error) and the liveness property G(request -> F grant), and why this distinction matters for verification.

Model answer: G(not error) is a safety property: it says something bad (error) NEVER happens. Any violation is witnessed by a finite prefix of execution reaching the bad state. G(request -> F grant) is a liveness property: it says something good (grant) EVENTUALLY happens after a request. Violations require infinite traces where the grant never arrives. Safety properties can be checked on finite executions, while liveness properties require reasoning about infinite behavior, making them fundamentally harder to verify.

This distinction affects model checking algorithms. Safety violations produce finite counterexamples (a path to the bad state). Liveness violations require finding infinite counterexamples, typically lasso-shaped: a finite prefix followed by a cycle that repeats forever without satisfying the liveness condition. The algorithmic machinery for detecting such cycles (nested DFS, accepting conditions of Buchi automata) is more complex than simple reachability analysis for safety.

Question 4

In CTL, what is the difference between AG p and EG p?

Model answer: AG p means 'on ALL paths, p holds Globally (at every state)' — p is true in every reachable state of the system. EG p means 'there EXISTS a path where p holds Globally' — there is at least one infinite execution where p is always true, though other paths may violate p. AG is a universal guarantee about all behaviors; EG is an existential claim about one possible behavior.

The path quantifiers A (for all paths) and E (exists a path) are what distinguish CTL from LTL. LTL formulas are implicitly universally quantified over paths (like AG), but CTL allows mixing A and E at every level of nesting. AG(EF p) — 'from every reachable state, there exists some path eventually reaching p' — is a natural CTL property with no LTL equivalent.