Deductive proofs of almost sure persistence and recurrence properties

Abstract

Martingale theory yields a powerful set of tools that have recently been used to prove quantitative properties of stochastic systems such as stochastic safety and qualitative properties such as almost sure termination. In this paper, we examine proof techniques for establishing almost sure persistence and recurrence properties of infinite-state discrete time stochastic systems. A persistence property ♢☐(P) specifies that almost all executions of the stochastic system eventually reach P and stay there forever. Likewise, a recurrence property ☐♢(Q) specifies that a target set Q is visited infinitely often by almost all executions of the stochastic system. Our approach extends classic ideas on the use of Lyapunov-like functions to establish qualitative persistence and recurrence properties. Next, we extend known constraint-based invariant synthesis techniques to deduce the necessary supermartingale expressions to partly mechanize such proofs. We illustrate our techniques on a set of interesting examples.