@article{gurevich1985the,
author = {Gurevich, Yuri and Shelah, Saharon},
title = {The Decision Problem for Branching Time Logic},
year = {1985},
month = {August},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/decision-problem-branching-time-logic/},
pages = {668-681},
journal = {Journal of Symbolic Logic},
volume = {50},
}