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

翻译：Knaster-Tarski定理将完备格上单调函数的最大不动点刻画为最大后不动点，这自然引出了所谓的共归纳证明原理，用于证明某个元素小于最大不动点（例如，提供互模拟等价性的证据）。其对偶原理用于证明某个元素大于最小不动点，与归纳不变量相关。本文我们提供了类似的证明规则，但用于证明某个元素大于最大不动点，或其偶情况下的小于最小不动点。该理论针对形如$\mathbb{M}^Y$的适合格上的非膨胀单调函数发展，其中$Y$是有限集，$\mathbb{M}$是MV-代数，并基于原始函数的有限近似构造。我们证明该理论适用于广泛实例，包括终止概率、度量迁移系统、概率自动机的行为距离以及互模拟等价性。此外，它使我们能够确定求解简单随机博弈的原创算法。