Graduate Thesis Or Dissertation

 

Deductive Verification of Infinite-State Stochastic Systems Using Martingales Public Deposited

https://scholar.colorado.edu/concern/graduate_thesis_or_dissertations/12579s38w
Abstract
  • The focus of this dissertation is the analysis of and verification of discrete time stochastic systems using martingales. Martingale theory yields a powerful set of tools that have recently been used to prove quantitative properties of stochastic systems such as stochastic safety. In this thesis, we focus on the analysis of qualitative trace properties of stochastic systems such as almost sure reachability and termination, persistence and recurrence. An almost sure reachability property F(T) states that with probability 1 the executions of the system reach a target set of states T. A qualitative persistence property FG(T) specifies that almost all executions of the stochastic system eventually reach the target set T and stay there forever. Likewise, a recurrence property GF(T) specifies that a target set of states T is visited infinitely often by almost all executions of the stochastic system.For each type of property, we present deductive reasoning techniques in the form of proof rules that rely on finding an appropriate certificate function to establish almost sure reachability, persistence and recurrence properties of infinite-state, discrete time polynomial stochastic systems.Next, we extend known efficient constraint-based and abstract interpretation-based invariant synthesis techniques to deduce the necessary supermartingale expressions to partly mechanize such proofs. We demonstrate that martingale certificates can serve as expectation invariants and generalize this idea to sets of mutually inductive expectation invariants. [object Object]Finally, we explore the connection between the properties of our martingale certificates and existing concentration of measure results to establish probability bounds on the quantitative version of these properties.
Creator
Date Issued
  • 2016
Academic Affiliation
Advisor
Committee Member
Degree Grantor
Commencement Year
Subject
Last Modified
  • 2019-11-14
Resource Type
Rights Statement
Language

Relationships

Items