Reachability in two-clock timed automata is PSPACE-complete
scientific article