一句话：提出证明元素高于最大不动点或低于最小不动点的证明规则，并用有限逼近与 MV-代数格统一处理概率/度量语义及随机博弈。
Knaster-Tarski 定理将最大不动点刻画为最大后不动点，由此得到余归纳证明原则；其对偶与归纳不变式相关。本文提出在精神上类似但方向相反的证明规则，用于证明元素高于最大不动点或低于最小不动点。理论针对 MV-代数 M 与有限集 Y 构成的格 M^Y 上的非扩张单调函数，通过构造原函数的有限逼近来实现。作者展示该理论适用于终止概率、度量迁移系统、概率自动机的行为距离和互模拟等例子，并能导出求解简单随机博弈的新算法。
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.
@article{paperbot2211,
title = {Fixpoint Theory -- Upside Down},
author = {Paolo Baldan and Richard Eggert and Barbara König and Tommaso Padoan},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 2},
year = {2023},
doi = {10.46298/lmcs-19(2:15)2023}
}