The decision problem for branching time logic
Yuri G. Gurevich, Saharon Shelah · Journal of Symbolic Logic · 1985
Abstract The theory of trees with additional unary predicates and quantification over nodes and branches embraces a rich branching time logic. This theory was reduced in the companion paper to the first-order theory of binary, bounded, well-founded trees with additional unary predicates. Here we prove the decidability of the latter theory.