On Computability of Logical Approaches to Branching-Time Property Verification of Programs

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.