Solving fixpoint equations is a recurring problem in several domains: the result of a dataflow analysis can be characterized as either a least or greatest fixpoint. It is well-known that bisimilarity - the largest bisimulation - admits a characterization as a greatest fixpoint and furthermore mu-calculus model-checking requires to solve systems of nested fixpoint equations.
Often, these fixpoint equations or equation systems are defined over powerset lattices, however in several applications - such as lattice-valued or real-valued mu-calculi - the lattice under consideration is not a powerset.
Hence we extend the notion of fixpoint games (or unfolding games, introduced by Venema) to games for equation systems over more general lattices. In particular continuous lattices admit a very elegant characterization of the solution.
We will also describe how to define progress measures which describe winning strategies for the existential players and explain how abstractions and up-to functions can be integrated into the framework.
(Joint work with Paolo Baldan, Tommaso Padoan, Christina Mika-Michalski) .[-]