Fixpoint Theory -- Upside Down

Knaster-Tarski's theorem, characterising the greatest fixpoint of a monotonefunction over a complete lattice as the largest post-fixpoint, naturally leadsto the so-called coinduction proof principle for showing that some element isbelow the greatest fixpoint (e.g., for providing bisimilarity witnesses). Thedual principle, used for showing that an element is above the least fixpoint,is related to inductive invariants. In this paper we provide proof rules whichare similar in spirit but for showing that an element is above the greatestfixpoint or, dually, below the least fixpoint. The theory is developed fornon-expansive monotone functions on suitable lattices of the form$\mathbb{M}^Y$, where $Y$ is a finite set and $\mathbb{M}$ an MV-algebra, andit is based on the construction of (finitary) approximations of the originalfunctions. We show that our theory applies to a wide range of examples,including termination probabilities, metric transition systems, behaviouraldistances for probabilistic automata and bisimilarity. Moreover it allows us todetermine original algorithms for solving simple stochastic games