LIRA 中快速 Ramsey 量子消去 (及其对存活性检查的应用)
计算机科学中的逻辑
2026-01-23 v2 形式语言与自动机理论
摘要
Ramsey 量子符最近被提出作为一种统一框架，用于处理涉及以无限克隆形式出现的程序验证中感兴趣的性质，这类性质无法在一阶逻辑中表达。其中包括存活性验证和单子分解性。我们提出了名为 REAL 的工具，实现了对存在线性算术理论中的 Ramsey 量子符高效消去，包括整数线性算术理论 (LIA)、实数线性算术理论 (LRA) 以及混合情况 (LIRA)。该工具支持方便的输入格式，是 SMT-LIB 格式的一个扩展，加入了上述理论中的 Ramsey 量子符。我们还展示了相对于原始原型的显著加速。作为应用，我们提供了从 FASTer（用于验证无限状态系统可达性输出格式）到我们扩展的 SMT-LIB 格式的自动转换，表明我们的工具如何将 FASTer 扩展到存活性检查。
关键词
引用
@article{arxiv.2511.05323,
title = {Fast Ramsey Quantifier Elimination in LIRA (with applications to liveness checking)},
author = {Kilian Lichtner and Pascal Bergsträßer and Moses Ganardi and Anthony W. Lin and Georg Zetzsche},
journal= {arXiv preprint arXiv:2511.05323},
year = {2026}
}