一句话：揭示多数将分支时间验证归约为逻辑问题的进路，其逻辑问题严格难于验证问题，唯一例外是带不动点的一阶算术有效性。
本文研究图灵完备语言中程序的分支时间性质验证问题的难度，以及求解该问题的逻辑方法。此类方法通常把验证归约为逻辑问题，例如带扩展的 Horn 子句可满足性。论文追问这些逻辑问题究竟与验证问题同等困难，还是严格更难。结果显示，大多数方法所用的逻辑问题远难于验证问题；唯一例外是带不动点算子的一阶算术的有效性判定。论文还回答了相关自然问题，如 Horn 子句扩展是否必要。
This paper studies the hardness of branching-time property verification of Turing-complete programming languages, as well as logical approaches to the verification problem. As these approaches reduce the verification problem to logical problems, e.g. the satisfiability problem of Horn clauses with certain extensions, it is natural to ask whether the logical problems are as hard as the verification problem or strictly harder. This paper reveals that logical problems used in most approaches are far more difficult than the verification problem; the only exception is the validity problem of first-order arithmetic with fixed-point operators. We also answers some other natural questions, for example, whether the extensions of Horn clauses are necessarily.
DOI 原文 ·
@inproceedings{paperbot5546,
title = {On Computability of Logical Approaches to Branching-Time Property Verification of Programs},
author = {Takeshi Tsukada},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394766}
}