Date of Award

Spring 1-1-2016

Document Type

Dissertation

Degree Name

Doctor of Philosophy (PhD)

Department

Computer Science

First Advisor

Sriram Sankaranarayanan

Second Advisor

Fabio Somenzi

Third Advisor

Aditya Nori

Fourth Advisor

Matthew Hammer

Fifth Advisor

Rafael Frongillo

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.

Share

COinS