Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs

TL;DR

The paper addresses verifying LTL specifications over imperative polynomial programs by introducing a unified family of sound and complete witnesses, enabling both verification and refutation. It connects LTL verification to Büchi automata, and develops a template-based synthesis procedure that constructs polynomial witnesses (EBRFs and UBRFs) for polynomial transition systems; the core reduction relies on Putinar’s Positivstellensatz to transform existential constraints into a quadratic programming problem solvable by SMT solvers. The approach is shown to be sound and semi-complete, with sub-exponential complexity for fixed polynomial degree, and an implemented prototype demonstrates effectiveness on linear and non-linear benchmarks beyond prior tools. This yields a practical, general framework for LTL model checking over polynomial programs, combining theoretical unification with scalable, automated witness synthesis and empirical validation. The work advances verification by enabling semi-complete, template-based certified reasoning for a broad class of dynamic systems, with potential extensions to heap-manipulating programs via numerical abstractions.

Abstract

We study the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (LTL). We first present novel sound and complete witnesses for LTL verification over imperative programs. Our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. We then consider LTL formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. For this setting, we provide an efficient algorithm to automatically synthesize such LTL witnesses. Our synthesis procedure is both sound and semi-complete. Finally, we present experimental results demonstrating the effectiveness of our approach and that it can handle programs which were beyond the reach of previous state-of-the-art tools.

Figures (3)

• Figure 1: An example program (left) and its transition system (right). Note that there is non-determinism at $l_1.$
• Figure 2: An NBW accepting $\texttt{G}\ \texttt{F}\ \mathit{at}(l_2)$ with gray accepting nodes (left) and the product of the transition system in Figure \ref{['example_ts']} and this NBW (right). A node labeled $i,j$ represents location $(l_i, q_j)$. Unreachable locations have been removed.
• Figure 3: An example finite path between two states $a$ to $b$ with its cycle-decomposition $(C, \beta)$, where square and diamond states specify the cycles in $C$ and the gray-scaled states specify $\beta$.

Theorems & Definitions (21)

• lemma thmcounterlemma: From LTL to Büchi Specifications, Proof in Appendix \ref{['proof:lm1']}
• definition thmcounterdefinition: EBRF
• theorem thmcountertheorem: Soundness and Completeness of EBRFs for EB-PA
• corollary thmcountercorollary
• definition thmcounterdefinition: UBRF
• theorem thmcountertheorem: Soundness and Completeness of UBRFs for UB-PA
• corollary thmcountercorollary
• theorem thmcountertheorem: Existential Soundness and Semi-Completeness
• theorem thmcountertheorem: Universal Soundness and Semi-Completeness
• proof