一句话：提出在线性整数/实数算术中消去 Ramsey 量词的多项式时间算法，并用于终止性等验证。
本文研究扩充 Ramsey 量词的 SMT，这类量词断言某公式诱导图中存在团，可用于程序终止（传递二元谓词的良基性）与一元可分解性。作者为 LIA、LRA、LIRA 给出消去 Ramsey 量词的新算法；对存在量化公式，算法多项式时间且输出线性大小。由此，上述理论中传递谓词的良基性判定可直接交由优化 SMT 求解器处理，并为若干无限状态系统（简洁计时系统、单计数器系统、单调计数器系统）提供终止性与活性验证的完备半算法及最优复杂度。论文还解决 LRA/LIRA 无量词片段中关系一元可分解性开放问题，证明其为 coNP 完全，并保证 Veanes 等通用算法终止。原型在微基准上取得积极实验结果。
We study Satisfiability Modulo Theories (SMT) enriched with the so-called Ramsey quantifiers, which assert the existence of cliques (complete graphs) in the graph induced by some formulas. The extended framework is known to have applications in proving program termination (in particular, whether a transitive binary predicate is well-founded), and monadic decomposability of SMT formulas. Our main result is a new algorithm for eliminating Ramsey quantifiers from three common SMT theories: Linear Integer Arithmetic (LIA), Linear Real Arithmetic (LRA), and Linear Integer Real Arithmetic (LIRA). In particular, if we work only with existentially quantified formulas, then our algorithm runs in polynomial time and produces a formula of linear size. One immediate consequence is that checking well-foundedness of a given formula in the aforementioned theory defining a transitive predicate can be straightforwardly handled by highly optimized SMT-solvers. We show also how this provides a uniform semi-algorithm for verifying termination and liveness with completeness guarantee (in fact, with an optimal computational complexity) for several well-known classes of infinite-state systems, which include succinct timed systems, one-counter systems, and monotonic counter systems. Another immediate consequence is a solution to an open problem on checking monadic decomposability of a given relation in quantifier-free fragments of LRA and LIRA, which is an important problem in automated reasoning and constraint databases. Our result immediately implies decidability of this problem with an optimal complexity (coNP-complete) and enables exploitation of SMT-solvers. It also provides a termination guarantee for the generic monadic decomposition algorithm of Veanes et al. for LIA, LRA, and LIRA. We report encouraging experimental results on a prototype implementation of our algorithms on micro-benchmarks.
@article{paperbot2663,
title = {Ramsey Quantifiers in Linear Arithmetics},
author = {Pascal Bergsträßer and Moses Ganardi and Anthony W. Lin and Georg Zetzsche},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632843}
}