Deciding full branching time logic by program transformation