= Conclusions <section-conclusions>

We have seen how common systems of fixpoint equations are, especially in model checking, and how we can characterize them using a particular parity game called the powerset game. We have also seen how the moves of this game can be reduced and efficiently expressed using a logic for upward closed sets, which also fits a local algorithm for solving the game. We have then considered a pair of algorithms for locally solving parity games based on strategies.

Our contribution has then been to adapt such algorithms to be used with the powerset game, in particular bridging the conflicting requirements of the two by converting the powerset game to a total parity game, generalizing subgames to consider a subset of edges rather than vertices. This also resulted in the need for a lazy generation of symbolic moves through formula iterators, which also required an adaptation of the simplification process of the corresponding formulas to work on such iterators. In this process we have also introduced a series of small optimizations, most notably the ability to compute play profiles while expanding, which avoids potentially expensive valuation steps. We have then implemented a tool based on our theoretical work, which we have compared against LCSFE, an existing implementation with similar ideas, showing that we have improved over it, in some cases even by orders of magnitude.

#heading(outlined: false, level: 2, numbering: none)[Future work]

Although the focus of the game characterization is to be as general as possible, which we have also shown by providing a formulation of bisimilarity using logic formulas, the performance is still quite questionable. A possible improvement in this area could be obtained by integrating different parity game algorithms while keeping the local approach, for example the recent quasi-polynomial algorithms @firstquasipoly @zielonkaquasipoly seems to be very good candidates for this.

There also seems to be a lot of room for smarter expansion schemes by combining the informations given by play profiles with symbolic formulas. In particular we believe it could be possible to simplify some formulas such that moves that lead to better improvements are preferred over those that do not. Ultimately the goal would be to include the most critical edges in the expansion as soon as possible, so that the optimal strategy becomes known earlier.

The use of a logic to express symbolic moves also suggests that it might be possible to use symbolic data structures like _Binary Decision Diagrams_ (BDDs) to represent them, possibly improving their efficiency. This might in turn open new possibilities to the usage of symbolic moves thanks to making them easier and faster to manipulate, especially in combination with the previous point.

Another challenge involves integrating up-to techniques @baldan_upto, possibly in a generic way, which could result in speed ups by orders of magnitude. However the problem of efficiently determining when to apply them is still open. We suspect that the previously mentioned use of BDDs might help with this though.

Finally, further work could be done on the adaptation of the different domains. Our $mu$-calculus and bisimilarity adaptations currently expect a full labelled transition system to be given ahead of time, which sometimes may be too prohibitive and more in general reduce the benefits of a local algorithm. However in principle this could be generated on the fly, avoiding the need to generate parts of the model that are not necessary. The implementation of more and varied domain, like for example the previously mentioned Łukasiewicz $mu$-calculus and abstract interpretation techniques, is also a possibility for further work to show the generality of the game characterization for solving systems of fixpoint equations.
