Research seminar: Recursive Timed Automata
Recursive Timed Automata (RTA) generalizes both Recursive State Machines and Timed Automata. This added power makes the problem of termination in RTA games undecidable. If we constraint function calls to be entirely pass-by-value or pass-by-reference, we get back the decidability of reachability and termination games.
Slides are available here.