AI 中文总结
针对含底元素的诺特偏序集上的方程组，提出基于依赖预言机的全局与局部算法，该方法灵活可定制，在不损害正确性的前提下权衡精度与性能，原型实现竞争力强且适配性好。
AI 中文摘要
我们提出了用于求解含底元素的诺特偏序集上方程组的全局与局部算法，该通用设定是诸多验证问题的基础。我们的算法通过将探索范围限制在确定所选变量值所需的系统部分，来计算该变量的解。我们借助依赖预言机计算变量依赖关系，以此实现这一目标。预言机引导系统探索过程，并为局部不动点计算提供可靠的终止准则。我们方法的关键优势在于其灵活性：预言机可定制、组合或过近似，为在不损害正确性的前提下，提供了一种权衡精度与性能的原则性方式。我们将我们的解决方案与文献中的现有算法进行对比评估，结果表明，我们的原型实现具有竞争力，且往往优于专用解决方案，同时保持简单性，并可在不同应用领域中适配。
英文摘要
We present global and local algorithms for solving systems of equations over Noetherian posets with a bottom element, a general setting underlying many verification problems. Our algorithms compute the solution of a selected variable by restricting exploration to those parts of the system required to determine its value. We achieve this by computing variable dependencies by means of dependency oracles. Oracles guide the exploration of the system and provide sound termination criteria for local fixed-point computation. A key advantage of our approach is its flexibility: oracles can be customized, composed, or over-approximated, offering a principled way to trade precision for performance without compromising correctness. We evaluate our solution against existing algorithms from the literature and show that our prototype implementation is competitive and often outperforms specialized solutions, while remaining simple and adaptable across diverse application domains.
