  Strategy iteration is a technique frequently used for two-player games in
order to determine the winner or compute payoffs, but to the best of our
knowledge no general framework for strategy iteration has been considered.
Inspired by previous work on simple stochastic games, we propose a general
formalisation of strategy iteration for solving least fixpoint equations over a
suitable class of complete lattices, based on MV-chains. We devise algorithms
that can be used for non-expansive fixpoint functions represented as so-called
min-, respectively, max-decompositions. Correspondingly, we develop two
different techniques: strategy iteration from above, which has to solve the
problem that iteration might reach a fixpoint that is not the least, and from
below, which is algorithmically simpler, but requires a more involved
correctness argument. We apply our method to solve energy games and compute
behavioural metrics for probabilistic automata.
