Branching Time Temporal Logic

Deciding branching time logic

We've been looking at temporal logics for the last couple of lectures in Software Quality Management which has lead me to think a bit about the semantics of CTL (Computation-time Temporal Logic), primarily because they weren't spelt out in the lectures and the first page of results from Google Scholar didn't look promising.

CTL is a logic used to reason about the characteristics of programmes over time. As such it needs to be able to analyse a particular "run" (i.e. a linear sequence of states). It must also be able to deal with the non-determinism present in many programmes. To do this it must be able to handle branching of the successor relation, i.e. a state having multiple possible successors.

CTL has 4 modal operators: A ("for all paths"), E ("for some path"), F ("sometime") and G ("always"). These four operators are always used in pairs: AF, AG, EF and EG. The AG operator is equivalent to a □ (the box or "necessary" operator) and the EF operator is equivalent to a ◇ (the diamond or "possible" operator).

After a bit of thought, I think I've nearly got the semantics worked out in my head. At interpretation of CTL would be a Kripke frame (some worlds and a relation on them) and a valuation function (giving the truth values for formulæ at worlds). The relation R is irreflexive and non-transitive. The modal operators that handle the branching (A and E) are interpreted with R. The linear-temporal modal operators (F and G) are interpreted with the reflexive and transitive closure of R.

This is the point I have reached. Having written this, I don't think I've fully understood the implications of F and G being linear. I'll need to go through it again. On the plus, this might be useful for my thesis: all I need to do is try to find a natural-looking way to find the correct semantics for CTL, whatever they may be, using counter-models for intended theorems of CTL. It is a fun exercise in any case.