Deductive Proofs of Almost Sure Persistence and Recurrence Properties Conference Proceeding uri icon



  • 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.

publication date

  • January 1, 2016

Date in CU Experts

  • January 28, 2016 4:38 AM

Full Author List

  • Chakarov A; Voronin Y-LV; Sankaranarayanan S

author count

  • 3

Additional Document Info

start page

  • TBA

end page

  • TBA


  • TBA