Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs

TL;DR

This paper demonstrates the computational hardness of finding the strongest polynomial invariants in loops, linking it to the long-standing Skolem problem, and introduces moment invariants for probabilistic programs.

Contribution

It establishes the hardness of computing strongest polynomial invariants for polynomial loops and introduces moment invariants for probabilistic programs, providing new insights and algorithms.

Findings

Strongest polynomial invariants are as hard to compute as the Skolem problem.

Strongest polynomial moment invariants are uncomputable or Skolem-hard in general.

A class of probabilistic loops with computable invariants is identified.

Abstract

We show that computing the strongest polynomial invariant for single-path loops with polynomial assignments is at least as hard as the Skolem problem, a famous problem whose decidability has been open for almost a century. While the strongest polynomial invariants are computable for affine loops, for polynomial loops the problem remained wide open. As an intermediate result of independent interest, we prove that reachability for discrete polynomial dynamical systems is Skolem-hard as well. Furthermore, we generalize the notion of invariant ideals and introduce moment invariant ideals for probabilistic programs. With this tool, we further show that the strongest polynomial moment invariant is (i) uncomputable, for probabilistic loops with branching statements, and (ii) Skolem-hard to compute for polynomial probabilistic loops without branching statements. Finally, we identify a class of probabilistic loops for which the strongest polynomial moment invariant is computable and provide an algorithm for it.