Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants f...
summary
Proves that computing the strongest polynomial invariant for single‑path loops with polynomial assignments is Skolem-hard, and that point‑to‑point reachability for discrete polynomial dynamical systems is also Skolem-hard via polynomial‑time reductions. Introduces moment invariant ideals for probabilistic programs, shows strongest polynomial moment invariant is uncomputable with branching and Skolem‑hard without branching, and identifies a syntactic class where invariants are computable, implemented by the Polar tool.
AI-written summary · about
chapters (10)
- 0:00Polynomial invariants intro
- 1:49Why polynomial invariants matter
- 3:33Computability in classical loops
- 4:36Hardness of loop invariants
- 6:21Skolem conjecture relation
- 9:30Invariants in probabilistic programs
- 11:12Moment invariant ideals
- 13:39Computability in probabilistic loops
- 15:45Summary of findings
- 16:26Q&A
related talks
30mThis Is the Moment for Probabilistic Loops
18mScalable Linear Invariant Generation with Farkas’ Lemma
29mQuantitative strongest post: a calculus for reasoning about the flow of quantitative inform
55mNon-commutative Computation
01h 22mTutorial 3: Geometric Invariant Theory
55mLower Bounds Against PC With Extension Variables
55mInequalities and Reductions for Nonzero Kronecker Coefficients
01h 19mTutorial 2: Algorithmic Invariant Theory