Timed Alternating Tree Automata: The Automata-Theoretic Solution to the TCTL Model Checking Problem. - Martin Dickhöfer; Thomas Wilke (ICALP, 1999)