2017, Thejaswini’s internship

On-the-fly algorithms for reachability and safety games need only explore a relevant part of the whole game graph, which often can be much smaller than the whole graph.  Thejaswini has improved an existing algorithm for reachability games. Then she has proposed two different on-the-fly algorithms for safety games. The first is based on repeatedly computing attractors and the second on finding Maximal End Components on the game graph. Both algorithms unfortunately have worst-case quadratic time complexity, while the standard (i.e., not on-the-fly) algorithm has linear complexity. These results have been written up in the form of a report.