A Local Algorithm for Systems of Fixpoint Equations: Study and Implementation

Many verification tasks, such as model checking of various kinds of specification logics, can be expressed via a system of (mixed) fixpoint equations over complete lattices. Recent contributions showed that the solution of systems of fixpoint equations have a game-theoretical characterisation in terms of a parity game. We call this type of parity game, built on top of a system of fixpoint equations, the powerset game. This game representation allows us to develop a local algorithm: we are particularly interested in finding the winner of the game from a specific position of the game graph (for example, for model checking, whether a state satisfies a formula). A naive implementation of the local algorithm could lead to the exploration of a uselessly large part of the game graph. We can reduce the number of moves, consequently shortening game play, thanks to the notion of selection, which intuitively selects a subset of best moves amongst all the possible moves. The main contribution of this thesis is an algorithmic overview of the powerset game, and a tool written in the language Rust. This tool is able to check whether a player has a winning strategy in the powerset game from a specific position, which formally corresponds to checking whether a lattice element is included in the solution of the system of fixpoint equations. It is our concern to ensure that the tool interoperates with the like of mCRL2 and Oink: this allows us to access a wide pool of examples as well as to compare our tool with the state of the art.