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 ⋄(T) states that with probability 1 the executions of the system reach a target set of states T. A qualitative persistence property ⋄□(T) specifies that almost all executions of the stochastic system eventually reach the target set T and stay there forever. Likewise, a recurrence property □⋄(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.
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.
|Commitee:||Frongillo, Rafael, Hammer, Matthew, Nori, Aditya, Somenzi, Fabio|
|School:||University of Colorado at Boulder|
|School Location:||United States -- Colorado|
|Source:||DAI-B 78/03(E), Dissertation Abstracts International|
|Keywords:||Formal methdos, Martingales, Stochastic systems, Verification|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be