一句话：提出多项式耦合与局部算法，高效计算多项式微分方程上的微分双模拟等价，并支持 up-to 技术与负例约束。
本文研究多项式微分方程这一动力系统模型上的等价关系计算，将概率双模拟提升为微分双模拟。作者提出多项式耦合概念，作为概率耦合的推广，并据此设计局部探索算法来计算等价关系。该算法具有多项式时间复杂度，可在不检查整个微分方程组的情况下得到等价，并可结合 up-to 技术增强，还允许指定不应出现在输出中的状态对。作者实现原型并在系统生物学案例中用于模型约简与比较；在反证 Markov 链等价时，运行时间比划分细化方法快四个数量级。
We introduce polynomial couplings, a generalization of probabilistic couplings, to develop an algorithm for the computation of equivalence relations which can be interpreted as a lifting of probabilistic bisimulation to polynomial differential equations, a ubiquitous model of dynamical systems across science and engineering. The algorithm enjoys polynomial time complexity and complements classical partition-refinement approaches because: (a) it implements a local exploration of the system, possibly yielding equivalences that do not necessarily involve the inspection of the whole system of differential equations; (b) it can be enhanced by up-to techniques; and (c) it allows the specification of pairs which ought not be included in the output. Using a prototype, these advantages are demonstrated on case studies from systems biology for applications to model reduction and comparison. Notably, we report four orders of magnitude smaller runtimes than partition-refinement approaches when disproving equivalences between Markov chains.
@inproceedings{paperbot6216,
title = {Efficient Local Computation of Differential Bisimulations via Coupling and Up-to Methods},
author = {Giorgio Bacci and Giovanni Bacci and Kim G. Larsen and Mirco Tribastone and Max Tschaikowski and Andrea Vandin},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470555}
}