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$( 提供两个不同的证人 ) 中适合的顶点的非爆炸性单调函数制定的 。 用于显示元素高于最大固定点( 确定) 和 $\ mathb{ M} 用于显示一个最小固定点的元素的双重原则 。 它基于原始功能的( 确定) 近似性) 的构造。 我们显示我们的理论适用于一系列广泛的例子, 包括终止性概率、 度过渡性过渡系统 、 行为距离, 使原始的游戏能够进行原始的亚性 。