不动点方程系统的抽象、up-to 技术与博弈
计算机科学中的逻辑
2021-06-21 v2
摘要
完备格上的不动点方程系统，由（混合的）最小与最大不动点方程组成，可用于表达若干验证任务，例如各类规范逻辑的模式检测或共归纳行为等价性的检验。本文以抽象解释的风格发展了不动点方程系统的近似理论：某个具体域上的系统被抽象为合适抽象域中的系统，并给出确保抽象解表示具体解的一个可靠/完全过近似的条件。有趣的是，up-to 技术——一种在共归纳设定中用于获得更简单或可行证明的经典方法——可被解释为抽象，从而自然契合我们的框架并推广到方程系统。此外，依托该近似理论，我们能用合适的奇偶性博弈刻画完备格上不动点方程系统的解，推广了近期仅限于连续格的一些工作。博弈视角为开发刻画此类方程系统解的按需（on-the-fly）算法开辟了道路。
引用
@article{arxiv.2003.08877,
title = {Abstraction, Up-to Techniques and Games for Systems of Fixpoint Equations},
author = {Paolo Baldan and Barbara König and Tommaso Padoan},
journal= {arXiv preprint arXiv:2003.08877},
year = {2021}
}