#let summary() = page[
  #v(1cm)

  = Summary

  #v(1cm)
  
  Fixpoint equations and, more generally, systems of fixpoint equations are ubiquitous in a number of formal verification tasks. This includes the model checking of specification logics, like the $mu$-calculus, and the check of behavioral equivalence, like bisimilarity. Consequently, a recurring problem consists in conceiving and implementing algorithms aimed at determining the solution of these systems. It has been shown in the literature that a game-theoretic characterization of the solution of equational systems can be given in terms of a parity game (a two-player, zero-sum game), which is referred to as fixpoint game or powerset game. The game view opens the way for the development of local algorithms for characterizing the solution of such equation systems. Two classes of algorithms can be identified: global algorithms, aimed at computing the full solution, by deciding the game for all positions, and local algorithms, which instead aim at determining only some "component" of the solution. For instance, in the case of the $mu$-calculus, of could be interested in checking whether a specific state enjoys or not a property, rather than determining all states satisfying the property. Similarly, for bisimilarity checking one might be interested in establishing whether two states are bisimilar, rather than computing the full equivalence.

  A local algorithm for solving a system fo fixpoint equations has been already proposed, based on the local algorithm for parity games due to Stevens and Stirling. In this thesis we explore the possibility of exploiting a different local algorithm for parity games, due to Vöge and Jurdziński, based on local strategy iteration. The idea is to start from arbitrary strategies for game players and progressively provide a local solution for systems of fixpoint equations. We show how this algorithm can be adapted to provide a local solution for systems of fixpoint equations. This is non-trivial as it requires, in particular, to deal with a symbolic representation of the moves of the game, and with a lazy generation of such symbolic moves. An implementation in the language Rust is also provided, and a comparison is conducted with other existing tools.
]
