Anne Schreuder

Automatic Synthesis of Polynomial Probabilistic Invariants via Geometric Persistence

FORSYTE/RiSE hosted a talk by Anne Schreuder

DATE:Monday, June 17, 2019
TIME:10:00 c.t.
VENUE:FORSYTE/RiSE seminar talk by Mateus de Oliveira Oliveira (U. Bergen,


We present an algorithm for the automatic synthesis of polynomial invariants for probabilistic transition systems. Our approach is based on martingale theory. We construct invariants in the form of polynomials over program variables, which give rise to martingales. These polynomials are program invariants in the sense that their expected value upon termination is the same as their value at the start of the computation. By exploiting geometric persistence properties of the system, we show that suitable polynomials can be automatically inferred using sum-of-squares optimisation techniques.


Laura Kovacs

Comments are closed.