Deductive Proofs of Almost Sure Persistence and Recurrence Properties | CU Experts

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 FG(P) specifies that almost all executions of the stochastic system eventually reach P and stay there forever. Likewise, a recurrence property GF(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 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.

VIVO