We give a sound and complete axiomatization for the full computation tree logic, CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.
['Mark Reynolds']
AN AXIOMATIZATION OF FULL COMPUTATION TREE LOGIC