*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
Title: Verification and Synthesis for Stochastic Systems with Temporal Logic Specifications
Committee:
Dr. Samuel Coogan, ECE, Chair , Advisor
Dr. Fumin Zhang, ECE
Dr. Ye Zhao, ME
Dr. Yorai Wardi, ECE
Dr. Kyriakos Vamvoudakis, AE
Abstract:
The objective of this thesis is to first provide a formal framework for the verification of discrete-time, continuous-space stochastic systems with complex temporal specifications. As these problems are generally undecidable or intractable to solve, approximation methods are employed in the form of finite-state abstractions arising from a partition of the original system's domain for which analysis is greatly simplified. The abstractions of choice in this work are Interval-valued Markov Chains (IMC) which, unlike conventional discrete-time Markov Chains, allow for a non-deterministic range of probabilities of transition between states instead of a fixed probability. Techniques for constructing IMC abstractions which rely on structural properties of the dynamics are presented for the class of mixed monotone systems and the class of polynomial systems. Next, an algorithm for computing satisfaction bounds in IMCs with respect to so-called omega-regular properties is detailed. As probabilistic specifications require finding the set of initial states whose probability of fulfilling some behavior is below or above a certain threshold, this method may yield a set of states whose satisfaction status is undecided. An iterative specification-guided partition refinement method is proposed to reduce conservatism in the abstraction until a precision threshold is met. Secondly, the approach developed for verification is extended to the synthesis of controllers that aim to maximize or minimize the probability of occurrence of temporal behaviors in stochastic systems. Similar interval-based finite abstractions are utilized to synthesize control policies for omega-regular objectives in systems with both a finite number of modes and a continuous set of available inputs. A notion of optimality for these policies is introduced and a partition refinement scheme is presented to reach a desired level of optimality.
