  In this paper we present methods for the 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. In order to guarantee this we
apply the Optional Stopping Theorem. Concretely, we present two approaches. The
first is restricted to linear systems. In this case under positive almost sure
termination there is a reduction to finding linear invariants for deterministic
transition systems. Secondly, by exploiting geometric persistence properties we
construct martingale invariants for general polynomial transition system. We
have implemented this approach and it works on our examples.

Logic in Computer Science