Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
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.
Thu 18 JanDisplayed time zone: London change
10:50 - 12:10 | |||
10:50 20mTalk | Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets POPL Nate Ackerman Harvard University, Cameron Freer Massachusetts Institute of Technology, Younesse Kaddar University of Oxford, Jacek Karwowski University of Oxford, Sean Moss University of Oxford, Daniel Roy University of Toronto, Sam Staton University of Oxford, Hongseok Yang KAIST; IBS | ||
11:10 20mTalk | Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures POPL Francesca Randone IMT School for Advanced Studies Lucca, Luca Bortolussi Department of Mathematics and Geosciences, University of Trieste, Emilio Incerto IMT School for Advanced Studies Lucca, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy | ||
11:30 20mTalk | Higher Order Bayesian Networks, Exactly POPL Claudia Faggian Université de Paris & CNRS, Daniele Pautasso Università di Torino, Gabriele Vanoni IRIF, Université Paris Cité | ||
11:50 20mTalk | Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs POPL |