COMING SOON! PQDT Open is getting a new home!

ProQuest Open Access Dissertations & Theses will remain freely available as part of a new and enhanced search experience at

Questions? Please refer to this FAQ.

Dissertation/Thesis Abstract

Deductive Verification of Infinite-State Stochastic Systems using Martingales
by Chakarov, Aleksandar Nevenov, Ph.D., University of Colorado at Boulder, 2016, 157; 10151160
Abstract (Summary)

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.

Indexing (document details)
Advisor: Sankaranarayanan, Sriram
Commitee: Frongillo, Rafael, Hammer, Matthew, Nori, Aditya, Somenzi, Fabio
School: University of Colorado at Boulder
Department: Computer Science
School Location: United States -- Colorado
Source: DAI-B 78/03(E), Dissertation Abstracts International
Subjects: Computer science
Keywords: Formal methdos, Martingales, Stochastic systems, Verification
Publication Number: 10151160
ISBN: 978-1-369-05924-3
Copyright © 2021 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy