一句话：在逻辑无关的抽象框架下，系统刻画循环证明无限下降检查准则的参数化复杂度，并提出改进算法。
循环证明系统通过隐式管理归纳，为自动验证提供了有前景的途径；其可靠性依赖于对循环证明图进行基于迹的无限下降性质检查。该检查已知为 PSPACE 完全，但文献中的循环证明系统采用了多种不同准则，其实际与参数化复杂度尚不清晰。本文在与具体逻辑无关的抽象框架下研究无限下降判定准则，重点分析基于 Büchi 自动机编码和关系抽象的准则，并以循环证明树的顶点数和顶点宽度（可同时追踪的 sequent 组件数上界）作为自然参数，给出参数化时间复杂度。作者识别出若干新算法，改进了现有算法的参数化复杂度，并实现这些准则，在多个基准上比较性能。
Cyclic proof systems, in which induction is managed implicitly, are a promising approach to automatic verification. The soundness of cyclic proof graphs is ensured by checking them against a trace-based Infinite Descent property. Although the problem of checking Infinite Descent is known to be PSPACE-complete, this leaves much room for variation in practice. Indeed, a number of different approaches are employed across the various cyclic proof systems described in the literature. In this paper, we study criteria for Infinite Descent in an abstract, logic-independent setting. We look at criteria based on Büchi automata encodings and relational abstractions, and determine their parameterized time complexities in terms of natural dimensions of cyclic proofs: the numbers of vertices of the proof-tree graphs, and the vertex width —an upper bound on the number of components (e.g., formulas) of a sequent that can be simultaneously tracked for descent. We identify novel algorithms that improve upon the parameterised complexity of the existing algorithms. We implement the studied criteria and compare their performance on various benchmarks.
@article{paperbot2619,
title = {The Complex(ity) Landscape of Checking Infinite Descent},
author = {Liron Cohen and Adham Jabarin and Andrei Popescu and Reuben N. S. Rowe},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632888}
}