The Decision Problem for Branching Time Logic

Define a tree to be any partial order satisfying the following requirement: if (y < x and z < x) then (y < z or y = z or y > z). The main result of the two papers [62, 63] is the decidability of the theory of trees with additional unary predicates and quantification over nodes and branches. This gives the richest decidable temporal logic.