*********************************
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. Coogan, Advisor
Dr. F. Zhang, Chair
Dr. Zhao
Abstract:
The objective of the proposed research is to design a scalable verification and synthesis tool for discrete-time, continuous-state stochastic systems subject to complex temporal logic specifications. In a stochastic framework, the verification problem amounts to finding the probability that a system exhibits a behavior of interest when initialized to some initial state; the synthesis problem requires designing a control policy that either maximizes or minimizes the probability that some specification is met. Our approach relies on finite-state abstractions of the underlying dynamics in the form of Interval-valued Markov Chains for systems without inputs and Bounded-parameter Markov Decision Processes for controlled systems, and we focus our attention on the expressive class of omega-regular specifications. The first goal of this work is to present classes of systems for which the aforementioned finite-state abstractions can be efficiently constructed given a partition of the continuous domain. Then, a computationally efficient automaton-based algorithm for verifying Interval-valued Markov Chains abstractions against omega-regular specifications has to be implemented, as well as a controller synthesis scheme for Bounded-parameter Markov Decision Processes with a finite or infinite set of inputs. Furthermore, as the optimality of the verification and synthesis algorithms with regard to the abstracted system depend heavily on the quality of the continuous domain partition, we aim to develop a specification-guided partition refinement procedure which targets regions of the state-space most likely to decrease the uncertainty in the abstraction until a precision threshold is reached. Lastly, this method should exploit all information obtained from coarser partitions to reduce computation times when re-performing verification or synthesis in the refined partitions and achieve enhanced scalability.
