Polynomial Probabilistic Invariants and the Optional Stopping Theorem

Anne Schreuder, C. -H. Luke Ong

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 invariant…