Optimising Parity Game Solvers using dynamic SCC maintenance

The mCRL2 toolset relies, for solving its model checking problems, on efficient algorithms for solving parity games. It is known that a decomposition into strongly connected components (SCCs) can help to speed up solving a parity game; in particular, a tight integration of an SCC decomposition in Zielonka's recursive algorithm for solving parity games allows it to solve important classes of games in polynomial time [1]. Currently, the SCCs need to be recomputed in each recursive call of the algorithm, which reduces its efficiency. However, there are efficient algorithms for maintaining SCCs under vertex and node addition/deletion [2]. 
In this assignment, you're asked to investigate the impact---both theoretically and practically---of using such dynamic SCC maintenance in Zielonka's algorithm. If successful and time permits, a follow-up study on applying similar ideas in the context of the various Priority Promotion [3] algorithms can be carried out.

[1] Maciej Gazda, Tim A. C. Willemse: Zielonka's Recursive Algorithm: dull, weak and solitaire games and tighter bounds. GandALF 2013: 7-20
[2] Aaron Bernstein, Maximilian Probst, Christian Wulff-Nilsen: Decremental strongly-connected components and single-source reachability in near-linear time. STOC 2019: 365-376
[3] Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero: Solving parity games via priority promotion. Formal Methods in System Design 52(2): 193-226 (2018)