Anne Schreuder

Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support

We study the synthesis of polynomial invariants for probabilistic transition systems (PTS) based on martingale theory. We present tractable methods to verify that such polynomials are indeed invariants, in the sense that their expected value upon termination is the same as their value at the start of the computation. W...