<p> 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 ⋄(<i>T</i>) states that with probability 1 the executions of the system reach a target set of states <i> T</i>. A qualitative persistence property ⋄□(<i>T</i>) specifies that almost all executions of the stochastic system eventually reach the target set <i>T</i> and stay there forever. Likewise, a recurrence property □⋄(<i>T</i>) specifies that a target set of states <i>T</i> is visited infinitely often by almost all executions of the stochastic system.</p><p> 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.</p><p> 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.</p>
| Identifer | oai:union.ndltd.org:PROQUEST/oai:pqdtoai.proquest.com:10151160 |
| Date | 10 January 2017 |
| Creators | Chakarov, Aleksandar Nevenov |
| Publisher | University of Colorado at Boulder |
| Source Sets | ProQuest.com |
| Language | English |
| Detected Language | English |
| Type | thesis |
Page generated in 0.002 seconds